« first day (1558 days earlier)      last day (1553 days later) » 

user400188
user400188
08:57
So, I have been thinking of the diagonal lemma for a while now, "A deductively defined theory $T$, which is able to represent every recursive function, will have the following property: For any predicate $B$, there is some $G$, such that $T\vdash B(\ulcorner G\urcorner)\iff G$."
Since we are able to choose any predicate $B$, it is often the case that we pick funny ones like "this statement is true" or "this statement is false". However it begs the question for me: What does it mean for a number (the Godel encoding of a statement) to be false?
user21820
user21820
09:54
@user400188 That's wrong. You cannot say "true" or "false".
Also, you need to be more precise, otherwise even your statement of the diagonal lemma is wrong.
Given any arithmetical theory T that can represent every computable function, and any predicate B over T, there is some sentence G over T such that T proves ( G ⇔ B(code(G)) ).
The point is, G is a sentence over T. It is not 'true' or 'false' in T.
code(G) is just a number, again not true or false.
And of course, "B(code(G))" actually means B(c) where c is the numeral (term of the form "0" or "1+...+1") representing code(G). That's why people use the corner-bracket notation, to allow directly applying B to the code of a sentence over T.
user400188
user400188
10:15
@user21820 Two questions, doesn't the theory $T$ also need to be deductively defined (possessing a finite or recursive set of axioms)? Also, what is meant by "over" here? I thought that the sentence $G$ (thank you for clarifying that it is a sentence, not just any wff) had be something which the theory $T$ could reason about. That is, the sentence $G$ was something that $T$ could express. "Over" makes it sound like $G$ isn't in the theory, but it's in the meta system about the theory.
user21820
user21820
@user400188 I don't think you need T to be computable, unless you want B to say something like "provable over T".
As for "over", I thought we went over that here before?
What are sentences over L are defined analogously to interpretations over L.
Anyway I need to go. The point is that G is not something that T reasons about; G is a sentence over the language of T.
user400188
user400188
Sorry to see you go, I'll have another look and that post from earlier and see what I can gather from it by replacing "interpretation" with "sentence".
Thank you for your continued help :)
user400188
user400188
10:48
I'm not sure if it is really analogous. Point (3) lists something that is only true for complete theories, if "interpretation" $I$ is replaced by "sentence" $S$: ( S ⊨ A+"∨"+B ) iff ( S ⊨ A ) or ( S ⊨ B ), for any formulae A,B. (Here I use an extended definition of satisfaction, where one wff can satisfy another if it implies it).
 
2 hours later…
user21820
user21820
12:35
@user400188 Err obviously you don't just replace "interpretation" by "sentence". At that time, I asked you to try defining "formula" and "sentence" rigorously, using the same kind of recursive definitions. It is much easier than defining "⊨"...
You should have tried it, so that I can see exactly what difficulty you are having with formal definitions.
 
1 hour later…
user21820
user21820
13:54
@user400188: Keep in mind that everything we talk about here are objects that we reason about in the meta-system, including T,B,G. We always work within the meta-system, unless otherwise stated.
And I think it's necessary to have 100% grasp of how to perform formal FOL deduction within the meta-system if you truly want to understand what is going on. You can do Fitch-style reasoning for PL (propositional logic), but you also need to be able to do Fitch-style reasoning for full FOL, and also need to know how precisely definitorial expansion works. Otherwise it will quickly become impossible to mentally grasp all that is going on in the study (not use) of FOL.
 
6 hours later…
user21820
user21820
19:35
Just to demonstrate, I will give a rigorous 1-page proof of the fixed-point lemma relying on basic FOL and the representability theorem and nothing else.
Let LA be the language of arithmetic. Define a numeral to be a term over LA that is either "0" or k+"+1" for some numeral k.
Given any FOL language L, define a 1-parameter sentence Q over L to be a formula over L with exactly one free variable.
For convenience, for any formula Q and term t over L, we write "Q(t)" to denote the string obtained by substituting every occurrence of the first free variable in Q by t.
Take any language L that extends LA, and any theory T over L that extends PA.
Let code be the Godel coding function for L, which maps each formula/term over L to its Godel code.
Let num be the numeral map, namely the function that maps each k∈ℕ to the numeral with exactly k "1"s.
Let sub be a computable substitution map such that sub(code(Q),k) = code(Q(num(k))) for every formula Q over L and k∈ℕ.
Let T' be the definitorial expansion of T with new function-symbol s that represents sub.
Take any 1-parameter sentence Q over L, and let v be an FOL variable that does not occur in Q.
For precision, we shall write string literals using escaping, where "[x]" in a string literal denotes the string x.
Let D = Q("[s]([v],[v])") and d = num(code(D)). // That is, D = Q( s+"("+v+","+v+")" ). This mimics D = ( v ↦ Q( v(v) ) ).
Then D is a 1-parameter sentence over T' with free variable v.
Let G = D(d) and g = num(code(G)). // This mimics G = ( v ↦ Q( v(v) ) ) ( v ↦ Q( v(v) ) ) = Q( ( v ↦ Q( v(v) ) ) ( v ↦ Q( v(v) ) ) ).
Then G is a sentence over T' and G = Q("[s]([d],[d])"), so T' trivially proves "[G] ⇔ [ Q("[s]([d],[d])") ]".
Also sub(code(D),code(D)) = code(G) by definition of sub, so T' proves "[s]([d],[d]) = [num(code(G))]" by definition of s.
Note that T' trivially proves "[t] = [u] ⇒ ( [Q(t)] ⇔ [Q(u)] )" for any terms t,u over T'.
Therefore T' proves "[G] ⇔ [ Q("[num(code(G))]") ]".
Thus T proves "[G] ⇔ [ Q("[num(code(G))]") ]" since T' is conservative over T.
user21820
user21820
In many logic textbooks, they use greek alphabetization as their escaping mechanism. In the above proof, everything is 100% explicit. Also, the usual approach (e.g. Rautenberg) is not to use definitorial expansion, but it just obscures the point.
user21820
user21820
19:56
The proof of course works for RA (Robinson Arithmetic) in place of PA as well, since the representability theorem holds for RA.
Observe that no computability restriction on T is required! Of course, if T is not computable, then you cannot construct a 1-parameter sentence Q over T that represents provability over T.
 
1 hour later…
Paulo Henrique L. Amorim
Paulo Henrique L. Amorim
21:22
Hello @user21820 Im the OP from the question math.stackexchange.com/questions/3912993/… you provided a comment relating my last paragraph non decidibility of TC, I have read you question and answer, but as beginner I had hard times to understand some parts because I just started my study on logic few days ago.
As I said in my question im going through the book Logic, Mathematics, and Computer Science: Modern Foundations with Practical Applications from Yves Nievergelt.

I noticed the only reviewer in amazon here(https://www.amazon.com/Logic-Mathematics-Computer-Science-Applications/dp/1493932225) quote the book of Rautenberg too.

I come here in Logic chat to ask you all if trying to learn first the Classical propositional logic then FOL in a formal way is a reasonable path to start to understand results from Godel like Incompleteness and to grasp the computability theory better seem to be a reas…

« first day (1558 days earlier)      last day (1553 days later) »