@Zophikel This example is a tricky one. I'm a native English speaker so it's easy for me.
"after all" indicates that it is the reason for the foregoing statement.
And "must have been" indicates that it is a conclusion.
@Zophikel Same explanation for this one.
@shredalert Lol I think pinging @everyone doesn't work. It would be nice though to be able to ping all users who 'subscribe' to the chat-room, perhaps those who mark it as favourite.
It's kind of a good and bad example at the same time. Good because it shows how messed up natural language can make the logical structure. Bad because it's messed up hahahaha..
Like what on earth does "after everything" got to do with reasoning? =P
Hopefully it pushes people to think more clearly about writings in real life.
For me it always results in me finding many plot holes in every fiction book I've read.
It was appropriately funny as well, and then I was thinking about the ambiguity of natural language and was laughing to myself. I think the person thought I was a bit of a nutter. lol
@user170039 I disagree with large portions of the linked paper. If you understood my explanations of circularity with regard to symbols, and that the best way we know today to achieve precision is via explicit computer programs (better still primitive recursive programs), then you can see that we're going to have to assume the meaningfulness of finite strings and these p.r. programs, as did logicians like Godel. If I recall right, Russell's theory of types with urelements (TSTU), is compatible.
@shredalert Hmm anything else more specific to you? Many people read novels haha..
@user170039: Anyone who disagrees with the meaningfulness of finite strings and p.r. programs is going to have to explain the incredible coincidence that HTTPS has always worked for every key pair thus used in history, which does seem to require philosophical commitment to the ontological meaningfulness of PA at least at scales accessible to us.
I was reading about $\alpha$-substitution yesterday. And I realised that some of the examples were correct but with multiple binding variables one has to do them one at a time if the definition is to be followed precisely.
@user170039: In fact I'm compelled to add that, after reading more of the PDF you linked to, I'm fairly convinced that the author does not actually understand the incompleteness theorems, much less give a valid criticism of it. If you understood them, you would also know what I mean.
I'm not too sure why Mauro didn't elaborate to give his own opinion, because it's certainly at odds with Boyce.
To be 100% precise, the following claim in the PDF is false:
> The system of Principia resists Gödel’s technique of arithmetisation and thus provides a viable classical theory of arithmetic.
Godel may have made minor mistakes or interpreted PM differently from others, but his ingenious β-function is the key to generalizing the incompleteness theorem to literally anything that can do basic arithmetic or finite string manipulation. You can read my proof of the incompleteness theorem for every conceivable precise practical formal system here (excluding the proof of properties of the β-funtion):
I've always interpreted this notion in the following way.
$
\def\eq{\leftrightarrow}
\def\t{\text}
\def\pa{\t{PA}}
\def\th{\t{Th}}
\def\prf{\t{Proof}}
\def\prov{\t{Prov}}
\def\box{\square}
\def\nn{\mathbb{N}}
\def\str#1{{``\text{#1}\!"}}
$
Formal system interpretation
Take any formal systems...
I know vaguely one of the completeness theorems says that not everything about first-order PA can be proved formally from the axioms. I don't know why someone would argue against that if they stick to classical logic.
Also, the following post gives a more layman account of the true extent of impact of the incompleteness theorems, including a brief description of a basic axiomatization of finite strings called the theory of concatenation devised relatively recently, which appears (but I'm not sure) to be weaker than PA− and yet suffers incompleteness:
You ask:
How can Peano ever be proved consistent?
Firstly, Peano is a person, and I'm certain that nobody can prove that he is consistent.
I assume you're asking for an absolute proof of consistency of (first-order) PA. That was more or less Hilbert's goal, namely to give a finitist proof...
@shredalert You mean "one of the incompleteness theorems"?
Vaguely, the first incompleteness theorem says that any nice formal system cannot prove some arithmetic fact about the natural numbers without being inconsistent.
Yes indeed that's the strength of the incompleteness theorems. As long as the meta-system has a collection of natural numbers (namely a structure that satisfies PA), that's enough.
It doesn't matter what on earth the formal system in question is, and whether it's illogical or not.
So one way to escape is to insist that there's no such thing as natural numbers after all, so that it's meaningless for it to be assumed to exist in the meta-system.
In case you're interested, here are the constructive versions of the incompleteness theorems:
1st: You can write an explicit program G1, that when given any formal system S that interprets arithmetic via I (a proof verifier program and a translator program), and given any proof P over S of I(Con(S)), will output a proof Q over S of I(false).
2nd: You can write an explicit program G2, that when given any formal system S that interprets arithmetic via I, outputs a proof Q over S of I(Prov(Con(S)⇒¬Con(S)).
It's as constructive as you can hope for. The proof of these constructive versions of course needs a bit of assumptions, but most practical type theories can do it.
@shredalert I got intrigued by the front cover, but alas it isn't natural deduction. =P
logic first order+ higher order -> discrete math -> analysis seems like a pretty good syllabus to me
That way students wouldn't complain about writing proofs more than half way into the course
And I'd say keeping the logic basic at the start, just enough to do mathematics with, is probably a good idea. Just give recommended reading to those who want to study it deeper.
So that way the engineers and physicists would actually enjoy their theoretical mathematics courses.
@shredalert I'm not sure if I have studied temporal, but I did have to study a form of boolean algebra in which the truth value of certain terms changed in time. (I think t was called a timing diagram)
Its way past the time that its appropriate, but in regards to how different exposition for the same topic can be, this wikipedia article here: https://en.wikipedia.org/wiki/Interpretation_(logic) Showcases a definition of "Addition" that looks completely unrelated to math in general. (its at the bottom under example).
In fact, I thought the definition was easy enough to understand, that it was appropriate to give to a prep or preschool class. In order to give them a rigorous definition of addition without scaring the parents.
By the way, I've been meaning to ask what is meant by Closure and concatenation here: https://math.stackexchange.com/questions/2206030/how-can-peano-ever-be-proved-consistent/2207370#2207370
@user400188 The concatenation of the strings "abc" and "xy" is the string "abcxy".
Closure of a collection S under a binary operation # means that ∀x,y∈S ( x#y∈S ).
First-order logic already inherently has the inbuilt assumption that every function-symbol represents an operation under which the collection of objects in the world is closed.
@user21820: I think that you are right. I also couldn't make sense of the part of the text that you quoted.
user131753
However noting that the author didn't sketched full details of the system that he is describing I thought that there must me something that I am missing (being no expert regrading PM and PM1925 also contributed to this thought).
user131753
The author seems to develop these ideas in more detail here.
@user170039 Thanks, but I think I'll pass. Unless someone shows a flaw with the incompleteness theorems (which I've myself proven), I just don't see a need to know what exactly the authors of PM were thinking. If their system is really not susceptible to the incompleteness theorems, then it necessarily must either be imprecise or unable to prove at least one true Π1-sentence of arithmetic, which is quite serious a problem, to say the least.
