A
B
/\I
A /\ B
A /\ B
/\E1
A
A /\ B
/\E2
B
A [a]
B
->I [a]
A -> B
A -> B
A
->E
B
A
\/I1
A \/ B
B
\/I2
A \/ B
A \/ B
A [a]
C
B [b]
C
\/E [a] [b]
C
trivial
True
False
absurd
C
A [a]
False
!I [a]
!A
!A
A
!E
C
LEM
A \/ !A
!!A
DNE
A
!A [na]
False
PBC [na]
A
(the syntax 't[a/x]' means 't' with 'a' substitute for 'x').
A[a/x]
ForallI [a]
forall x . A
forall x . A
ForallE
A[t/x]
A[t/x]
ExistsI
exists x . A
exists x . A
A[a/x] [u]
C
ExistsE [a] [u]
C