^^Proof system ≡ logical calculus.

≡ logical calculus (of the formal system)

Argomento della pagina

da ignorante di logica, io qui vorrei "come fare una dimostrazione-deduzione seconde le regole della logica", cioe' la base del sistema ipotetico-deduttivo, cioe' come fare a dedurre in modo logico, senza errori di logica.

La mia pagina ingenua sulla dimostrazione e'

Dimostrazioni; 3 tipi. Serie di implicazioni, contrapositivo, assurdo.

proof system is to prove statements.

Consists of 3 components

Linguaggio formale.
Rules of inference: List of rules that can be employed to prove theorems from axioms and theorems.
Axioms: Formulas in L assumed to be valid.

e' componente di un sistema di logica.

A proof system: sound, complete

soundness and completeness

sound

everything provable is true

only true things are provable

if provable then is true

if φ1, …, φn ⊢ ψ then φ1, …, φn ⊨ ψ.

complete

everything true is provable

only provable things are true

if true then is provable

if φ1, …, φn ⊨ ψ then φ1, …, φn ⊢ ψ.

"truth" (⊨) and "provability" (⊢) have separate definitions

provability (⊢)	depends on the proof system
truth (⊨)	depends on the semantics

have separate definitions.

We would like them to be the same, a sound and complete system.

How can we connect derivability and truth?

In propositional logic, what is true depends on the truth assignment.
In first-order logic, truth depends on the interpretation.

styles of proof system

Trees

axiomatic systems of logic

are not very nice to work with, and don't reflect the natural ways of reasoning used in common sense deductive reasoning (e.g. in mathematical proofs

Natural deduction systems

By contrast natural deduction systems are intended to reflect much more closely those natural ways of reasoning, by encoding the sort of inference moves that we ordinarily make, and giving us a regimented framework for setting out arguments using these moves.
Core features

no axioms and lots of rules of inference, rather than
lots of axioms and just one or two rules of inference
- crucially - allowing suppositional proofs, in which some proposition is temporarily assumed for the sake of argument and then the assumption is later `discharged' (as, for example, in a reductio proof).

A natural deduction system in pretty much the modern form was proposed by
Gerhard Gentzen in his doctoral thesis of 1933.

Constructive proofs and computation

there is a deep relationship between them

the "Curry-Howard isomorphism" or formulae-as-types principle.

upenn/proofslambda.pdf pag. 63