by Peter Smith
is1931 Gödel's great paper. Understanding the paper title:
system axiomatized theory effectively axiomatized formal theory
naif: 1: you fix on a formalized language; 2: set down some axioms stated in
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
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.
Note: a language, for us, has both a syntax and an intended semantics:
syntactic rules fix which strings of symbols form
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.
terms sentences well formed formulas
bound of ubnound variables
wff well formed formula