Om premisser i bevis

Indentering i beviser brukes for å skille ut det boken kaller delbeviser (subproofs); det vil si at man for en stund gjør en ekstra antakelse og ser hvor den fører hen. Den ekstra premissen og formlene man får fra den står på linje under hverandre med samme indentering. Avhengigheten av premisset kan fjernes ved bruk av den spesielle regelen CP. At avhengigheten er borte, angis ved at den nye formelen ikke får samme indentering.

Av og til kan det være nyttig å ha en mer eksplisitt oversikt over hvilke premisser de enkelte formlene i beviset avhenger av. Bevisene på de neste sidene har fått en ekstra kolonne til høyre hvor vi holder greie på hvilke premisser formelen i hver linje avhenger av. (Premissene identifiseres ved sine linjenumre.)

(1) A → A

\begin{matrix}1  A & P & 1 \\ 2  A → A & 1,1,CP \end{matrix}

(2) A ∧ ¬A → false

1  A ∧ ¬A  P  1
2  A  1,Simp 1
3  ¬A  1,Simp 1
4  false ∨ A  2,Add 1
5  false  4,3,DS 1
6  A ∧ ¬A → false  1,5,CP

(3) ¬¬A → A

1  ¬¬A  P  1
2  A ∨ ¬A  XM
3  A  2,1,DS 1
4  ¬¬A → A  1,3,CP

(4) A → ¬¬A

1  ¬¬A → ¬¬A  T fra (1) over
2  A ∧ ¬A → false  T fra (2) over
3  A  P  3
4  ¬A  P  4
5  A ∧ ¬A  3,4,Conj  3,4
6  false  2,5,MP  3,4
7  ¬¬A  6,FE  3,4
8  ¬A → ¬¬A  4,7,CP  3
9  ¬A ∨ ¬¬A  XM
10  ¬¬A ∨ ¬¬A  9,8,1,CD  3
11  ¬¬A  10,Contr  3
12  A → ¬¬A  3,11,CP

Flere beviser

1  A → B  P  1
2  ¬A → B  P  2
3  A ∨ ¬A  XM
4  B ∨ B  3,1,2 CD 1,2
5  B  4,Contr 1,2
6  (¬A → B) → B  2,5,CP  1
7  (A → B) → ((¬A → B) → B)  1,6,CP

1  A  P  1
2  B  P  2
3  A ∧ B  1,2,Conj 1,2
4  B → (A ∧ B)  2,3 CP 1
5  A → (B → (A ∧ B))  1,4,CP

1  A ∧ B  P  1
2  A  1,Simp 1
3  A ∧ B → A  1,2,CP
4  ¬A  P  2
5  ¬(A ∧ B)  3,4,MT 2
6  ¬A → ¬(A ∧ B)  1,5,CP

1  A ∧ B  P  1
2  B  1,Simp 1
3  A ∧ B → B  1,2,CP
4  ¬B  P  4
5  ¬(A ∧ B)  3,4,MT 4
6  ¬B → ¬(A ∧ B)  1,5,CP

1  true  TI

1  ¬false → ¬false  T fra (1) over
2  false  P  2
3  ¬false  2,FE  2
4  false → ¬false  2,3,CP
5  false ∨ ¬false  XM
6  ¬false ∨ ¬false  5,4,1,CD
7  ¬false  6,Contr

1  A ∧ ¬A → false  T fra (2) over
2  ¬A  P  2
3  A  P  3
4  A ∧ ¬A  3,2,Conj  2,3
5  false  1,4,MP  2,3
6  B  5,FE  2,3
7  A → B  3,6,CP  2
8  ¬A → (A → B)  2,7,CP

1  B  P  1
2  A  P  2
3  B ∨ B  1,Add 1
4  B  3,Contr 1
5  A → B  2,4,CP 1
6  B → (A → B)  1,5,CP

1  A  P  1
2  A → B  P  2
3  B  MP  1,2
4  (A → B) → B  2,3,CP 1
5  ¬B  P  5
6  ¬(A → B)  4,5,MT 1,5
7  ¬B → ¬(A → B)  5,6,CP 1
8  A → (¬B → ¬(A → B))  1,7,CP

1  A  P  1
2  A ∨ B  1,Add 1
3  A → (A ∨ B)  1,2,CP

1  B  P  1
2  A ∨ B  1,Add 1
3  B → (A ∨ B)  1,2,CP

1  ¬A  P  1
2  A ∨ B  P  2
3  B  2,1,DS 1,2
4  (A ∨ B) → B  2,3,CP 1
5  ¬B  P  5
6  ¬(A ∨ B)  4,5,MT 1,5
7  ¬B → ¬(A ∨ B)  5,6,CP 1
8  ¬A → (¬B → ¬(A ∨ B))  1,7,CP