^^Gödel Without (Too Many) Tears.

by Peter Smith

www.logicmatters.net/2020/09/01/godel-without-tears-slowly-1

"On formally undecidable propositions of Principia Mathematica and related systems I"

is1931 Gödel's great  paper. Understanding the paper title:

1. 'I' paper first part
2. ? "formally undecidable proposition"
3. ? Principia Mathematica ?  book  by A. N. Whitehead and Bertrand Russell.
   1. What is the project of that book?
   2. what counts as 'related system' – a 'system' suitably related, that is, to the one in Principia?
   3. what is meant by 'system' here?
       

system     axiomatized theory     effectively axiomatized formal theory

1. effectively formalized language
2. effectively decidable set of axioms
3. effectively formalized proof-system

naif: 1: you fix on a formalized language; 2: set down some axioms stated in that language;
3: specify some apparatus for formally deriving results from your axioms; and there you have a theory.

first, the new idea to get is the

def1  intuitive notion of effective decidability

algorithm

a finite set of instructions for a deterministic computation

property

defined over some domain D of objects o

property effectively decidable

exists an algorithm for settling whether any object o∈D has property P,
in a finite number of steps

a set Σ is effectively decidable

the property of being a member of that set is effectively decidable.

cio' riporta  ‘effectively decidable’  a  ‘computably decidable’,

cioe' una visione computazionale, ora da formalizzare.

Non e' l'unica visione, ma si e' dimostrato che le diverse visioni formalizzate si equivalgono.

formalized language L

Note: a language, for us, has both a syntax and an intended semantics:

syntactic rules fix which strings of symbols form

1. terms
2. wffs
3. sentences closed wffs with no unbound variables dangling free

semantic rules assign unique interpretations
    interpretations assignments of truth-conditions to every sentence of the language.

It is not at all unusual for logic books to call a system of uninterpreted strings of symbols a ‘language’.

But I really think we should deprecate that usage.
Sometimes below I’ll talk about an ‘interpreted language’ for emphasis: but strictly speaking – in my idiolect – that’s redundant.

The familiar way of presenting the syntax of a formal language is by

(a) specifying some finite set of symbols, and then giving rules for building up expressions from these symbols.

And we standardly do this in such a way that

(b) we can effectively decide whether a given string of symbols counts as a term or wff or a wff with one free variable or a sentence (we can give algorithms which decide well-formedness, etc.).

(c) we can use the semantic rules to mechanically work out the interpretation of any given sentence.

constructional history (of a sentence)

the way it is syntactically built up from its parts

proof system    deductive apparatus

da sentenze si possono derivare altre

Talk

terms  sentences   well  formed formulas

bound of ubnound variables

well-formedness,

wff well formed formula

syntactic rules

fix which strings of symbols form

1. terms
2. wffs

3. sentences

   closed wffs with no unbound variables dangling free

semantic rules

assign unique

interpretations

assignments of truth-conditions to every sentence of the language.

spinoza montaigne