Primitive Rules of Proof

turnstile |- read as therefore

sequent arguments in formal notation

proof sequence of lines containing sentences that are either assumptions or the result of applying a rule of proof. Line of proofs contains annotation, assumption set, line number.

assumption A anything may be assumed at any time

ampersand-intro m, n & I Given two sentences at lines m and n, conclude a conjunction of them

arrow introduction