talanum1
Senior Member
- Jul 21, 2025
- 139
- 11
- 56
See thread: "Proof of "Axioms" of Propositional Logic: Synopsis" for the meaning of the symbols.
We have the axiom (A:O): (p)-(+)-( )-(+)-(~p) <-> (), where "()" is the empty structure which evaluates to "false".
From this we can prove: p, ~p OR C -> C as follows:
Line # Statement Reason
1 p ~p-(+)-C Premise
2 (p)-(+)-( (~p-(+)-C)-(+)-( 1, A:AtI
3 (p)-(+)-( )-(+)-(~p) []-(+)-(C)-(+)-( 2, A:AD
4 (_) []-(+)-(C)-(+)-( 3, A:O
5 false []-(+)-(C)-(+)-( 4, Evaluate (_)
6 false )-(+)-(C)-(+)-[] 5, A:ASS
7 false )-(+)-(C) 6, A:SD
8 C 7, A:ONT
Now (p)-(+)-(~p) is true, while we need to let the first 2 literals in line 3 to evaluate to "false" in order to conclude that C is true.
One may reason that (p)-(+)-(~p) <-> (p)-(+)-( )-(+)-(~p) by A:AL
We have the axiom (A:O): (p)-(+)-( )-(+)-(~p) <-> (), where "()" is the empty structure which evaluates to "false".
From this we can prove: p, ~p OR C -> C as follows:
Line # Statement Reason
1 p ~p-(+)-C Premise
2 (p)-(+)-( (~p-(+)-C)-(+)-( 1, A:AtI
3 (p)-(+)-( )-(+)-(~p) []-(+)-(C)-(+)-( 2, A:AD
4 (_) []-(+)-(C)-(+)-( 3, A:O
5 false []-(+)-(C)-(+)-( 4, Evaluate (_)
6 false )-(+)-(C)-(+)-[] 5, A:ASS
7 false )-(+)-(C) 6, A:SD
8 C 7, A:ONT
Now (p)-(+)-(~p) is true, while we need to let the first 2 literals in line 3 to evaluate to "false" in order to conclude that C is true.
One may reason that (p)-(+)-(~p) <-> (p)-(+)-( )-(+)-(~p) by A:AL
Last edited:
