From this page: https://www.reddit.com/r/math/comments/56bbd3/what_does_it_mean_for_something_to_be_true_but/
I have the following quote:
When we say true, we mean true of a particular structure. When we say provable, we mean provable from some axioms.
My questions are:
(1) what is the meaning of particular structure?
I guess it is a specific one.
(2) what is the meaning of some axioms?
I guess they are all depend on the set of positive integers.
On
Raymond Smullyan likes to frame this problem as an accurate and consistent logician who doesn't know that he is accurate or consistent visiting one of those islands where some of the people always tell the truth and the rest always lie. Imagine a native coming up to the logician and saying "You will never be able to prove that I am a truth-teller".
You and I looking at this problem can tell that the native is a truth-teller -- if he were a liar, then the logician would be able to prove that he was a truth-teller, which violates his accuracy. But from the logician's perspective, he will remain undecided about the native's reliability, because he doesn't have the perspective to know his own accuracy.
So, as far as provability goes, the reasoner's logic is like the axioms of a particular logical system, and our logic is like the axioms of a meta-system that is able to prove things about the simple system that it can not prove about itself.
And truth.... In a way, I'm glad I didn't formally study logic far enough to get to Tarski's theorem. Godel was head shaking enough, but (to coin a phrase) we can't handle the truth about Truth.
On
There are mathematical conjectures of the form: "there is no natural number with property x" that where shown to be undecidable and hence unproveable within standard axiomatic models of maths. But knowing that such a statement is unproveable immediatly implies that it is true because if it where false one could easily prove so by giving a counter example.
This question sums up the distinction between syntax and semantics. Proof is a syntactic notion, truth is semantic. Syntax concerns formal theories, semantics concerns structures.
In the simplest cases, a formal theory consists of a finite set of symbols (the vocabulary), plus rules specifying when a string of symbols is syntactically correct (a so-called formula), which formulas are axioms, and when a formula follows from other formulas (rules of inference). Key point: all this should be purely mechanical, and in principle programmable. Example: $$\forall x\exists y(x\cdot y=1)$$ is an axiom in the formal theory of groups.
A formula in a formal theory is provable if there is a finite list of formulas, such that every formula in the list is either an axiom, or follows by a rule of inference from earlier formulas on the list.
To define the notion of structure, we need a bit of set-theory. A structure for a theory consists of a set called the domain (or universe) of the structure, and enough relations, functions, and individuals in this domain to give meaning to the formulas of the theory. For example, a structure for the formal theory of a group consists of a set $G$ and a function $G\times G\rightarrow G$ (an 'operation') that interprets the symbol '$\cdot$' of the theory; also an individual element of $G$ that interprets '1'.
Tarski gave a definition of 'truth' (or 'satisfaction') for a class of theories known as first-order theories. If $T$ is a first-order theory, and $S$ is a structure for it, then Tarski defined the notion of "$\varphi$ is true in $S$", where $\varphi$ is a formula of $T$ (strictly speaking, a so-called closed formula of $T$).
If all the axioms of $T$ are true in a structure $S$, we say $S$ is a model of $T$.
Tarski's definition is inductive, i.e., truth for longer formulas is defined in terms of truth for shorter formulas. For example $\varphi\&\psi$ is defined to be true in $S$ if and only if both $\varphi$ and $\psi$ are true in $S$.
I'm leaving out gobs of details, which can be found easily in a zillion textbooks (or in my notes Basics of First-order Logic at diagonalargument.com). But I should add a few more generalities.
First, it's not possible to "get off the ground" without relying on an informal level of understanding. For example, Tarski's formal definition of the meaning of '$\varphi\&\psi$' assumes you understand the meaning of the word 'and'. Likewise, a certain amount of informal set theory must be taken for granted. (Set theory itself can be formalized as a first-order theory, but that doesn't erase the issue, just pushes it one level back.)
Second, the most famous example of a "true but unprovable" statement is the so-called Gödel formula in Gödel's first incompleteness theorem. The theory here is something called Peano arithmetic (PA for short). It's a set of axioms for the natural numbers. The so-called standard model for PA is just the usual natural numbers with the usual operations of addition and multiplication and the usual individual elements 0 and 1.
The Gödel formula cannot be proved in PA (if PA is a consistent theory, which most mathematicians believe). But you can give a convincing argument that the formula is true in the standard model. This proof of this argument uses notions from set theory, and cannot be formalized in PA. It can be formalized in other formal theories, however.