Meta-Reasoning Flashcards
Define Meta-Reasoning:
Reasoning about formal systems
Why is decidability important property axiomatic theories?
Can you decide whether a given wff is a theorem?
(If yes), we can determine what formulas are in the theory
A formal system with only lengthening rules is decidble!
What are Lengthening Rules?
Alphabet: a, b
Axiom: a
Rules:
1. x -> a x a
2. x -> b x b
Theorems: a, aaa, bab, aaaaa, ababa …
Difficult see theory is in THM since you have to look at N0
Hence, Is aaaa a theorem?
No!
Justification: aaaa not listed among theorems and any application rules makes formula longer, so aaaa cannot be among them
Therefore, A formal system with only lengthening rules is decidble!
Define Godel numbers:
An interpretation of the wff of a formal system as natural numbers.
“Coding” in the formal systems in arithmetic
See the relation between different lines arithmetically, as relations between natural numbers.
How do Godel numbers have a “dual nature?”
Can be treated typographically as numerals or arithmetically as numbers
Difference between numerals and numbers:
Syntax and semantics
Godel Numbers:
Typographical Rule 01:
From any theorem whose rightmost symbol is “1” a new theorem can be make by appending “0” to the right of that “1)
Syntactic Rule (Symbols, numerals)
Godel Numbers:
Arithmetical Rule 1b:
A number whose remainder when divded by 10 is 1, can be multiplied by 10
Semantic rule (numbers)
What is the Central Proposition:
Typographical rules for manipulating numerals are actually arithmetical rules for
operating on numbers.
CENTRAL PROPOSITION: If there is a typographical rule which tells how certain
digits are to be shifted, changed, dropped, or inserted in any number represented
decimally, then this rule can be represented equally well by an arithmetical counterpart which involves arithmetical operations with powers of 10 as well as additions, subtractions, and so forth.
What are the three levels of interpretation?
- Formal System
- Arithmetization
- Formal System
What is Arithmetization (Godel Numbering)?
Formal System (syntax) to Arithmetic (semantics)
Can use numbers (arithmetic) to talk about formal systems (such at MIU/TNT)
What are producible numbers?
Ex: MIU-producible numbers are Godel numbers of the theorem of the MIU system
Producible numbers - R.E. (because the theorems of formal systems are r.e.)
What is formalization?
From arithmetic to FOA
How does Godel numbering and formalization work from the MIU system to the FOA system?
x - not provable, but MON(x) is provable (formula) = prove the formula and not the term
However, not a decision procedure: a formula is not a procedure
What is MU-Mon(x)?
a) A FOA-string, resulting from stranslating ‘30 is a MIU-number’
b) A code for ‘MU is a theorem of the MIU-system”
How does Godel numbering and formalization work from the FOA system to the FOA system?
TNT can speak about itself
How can you find a sentence G in FOA that expresses a property about itself?
