natural deduction verificationism (~1930s) not allowed to define falsehood, to claim that something is falsejudgments: A true A false A provable A irrelevant A true at time t ...introduction rule - introduces foo in the conclusion not present in the premises. conjunction introduction (^I), disjunction introduction (vI) truth introduction has no premise (TI) there is no falsehood introductionprinciple: the meaning of a proposition must be defined from the meaning of its parts.elimination rule A^B true => A true A^B true => B true derived from ^I there is no top elimination rule - put no info in, get no info out. disjunction elimination? AvB true, assume-u A true ... C true, assume-w B true ... C true => C true bottom elimination: bottom true => C true implication elimination: A->B true, A true => B truenotational definition: A<->B = (A->B)v(B->A)