IA038	Types and	Proofs
3.	Natural Deduction
Jiří	Zlatuška
March 7, 2023
Notation for	proofs:	from	Frege	to	Hilbert	school
• Notation for judgements evolved into
⊢ A as the	judgement	that	A	is	asserted
• Modus	Ponens and axiom schemes:
B	implies A
B	is	asserted
A	follows
• Frege	started with	
pictorial notation
for	judgements
Modus	Ponens:	
Gentzen’s notation and	rules	for	Natural deduction
• Gentzen introduced	judgements	with	assumptions,
B1,	…,	Bn ⊢ A					meaning	A	proved	from	assumptions	B1,	…,	Bn
• Modus Ponens in Gentzen’s system:
here	Γ and ∆ are lists of propositions, Γ, ∆ means union of two lists (here just as
finite sets)
Gentzen’s rules	for	Natural	deduction
Gentzen’s tree	notation:
Example	proof
Gentzen’s rules	for	Natural	deduction
Modern	notation	(Prawitz,	Girard,	…):
Example	proof
[													] [						 ]
Proof	simplification