Please enable JavaScript.
Coggle requires JavaScript to display documents.
Box Proofs - Coggle Diagram
Box Proofs
-
The “Implication game”
2 rules:
Implication elimination rule
A--> B
Derive A, the result is B
Implication-introduction
If you derive B under the assumption of A, it will become A-->B.
only works with tutologies
-
if you are the same character again, say from line 1 you would say hypothesis 1 (hyp 1) or line 1.
is it not possible?
not if it has a counter example
line x cannot be justified bc how can u know if (letter) is true.
-
(E-->F) -->G) --> (F --> (E--> G))
The principal connective
A --> (B --> A)
The principal logic
The last line of the proof, the statement you are trying to prove.
The box proof always starts with an assumption (the top line is a letter).
-
-
The “not game”
notes contradiction ⊥
A ⊢ ¬¬ A (does not mean A ⊢ A)
You need to arrive to a conclusion and negate it to arrive to the target (this is called showing a contradiction).
Everything in the imaginary world (the box) must be a contradiction (cannot be true). So if we start with the assumption of ¬X and then add the premise X, this is a contradiction, so we add a not elimination of those two lines on the third line (sometimes called a contradiction rule).
On the very last line we add a not in front of the assumption because it is not true (which we have just proved). Therefore, if the assumption was ¬X then the last line will be ¬¬X.
-
-
-
The double negatyon rule
notes
this is not a valid rule it is a special rule
read it aload! "not, not X" sounds likes X.
⊥ is not provable.
Box proofs are a much more efficient way to show tautologies and is a clearer way to handle many variables.