Hilbert Proof System Definition Let 2 be a set of propositions A proof from∑ is a finite sequence a1,a2,…,an such that for each i< n either ③a; is a member of∑ ②a; is an axio o a; can be inferred from some of previous a by an application of a rule of inference o a is provable from∑,∑FHa, if there is a proof a1,Q2,…, an from∑ where an A proof of a is simply a proof from the empty set 0; a is provable if it is provable from 0Hilbert Proof System . Definition . . Let Σ be a set of propositions. 1. A proof from Σ is a finite sequence α1, α2, . . . , αn such that for each i ≤ n either: .1 αi is a member of Σ. .2 αi is an axiom; or .3 αi can be inferred from some of previous αj by an application of a rule of inference. 2. α is provable from Σ, Σ ⊢H α, if there is a proof α1, α2, . . . , αn from Σ where αn = α. 3. A proof of α is simply a proof from the empty set 0; α is provable if it is provable from 0. Yi Li (Fudan University) Discrete Mathematics April 16, 2013 16 / 17