27

I like to think that mathematical truth is a mathematical model of "real world truth", similar in my mind to the way in which the mathematical real number line $\mathbb{R}$ is a mathematical model of a "real world line", and similarly for many other mathematical models. In order to achieve the level of rigor needed to do mathematics, sometimes the ...


22

This kind of question often includes several common points of confusion. Confusing point 1: we cannot talk rigorously about a statement being "unprovable" without reference to the formal system for doing the proof. There is a mathematical, formally defined relation of provability between a formal system and a sentence, which defines what it means for the ...


12

We definitely care that formal logic has a formal semantics. Here's a list of reasons why. More simply, we need to know very precisely what a formalism means. Without this precise definition, there's a lot of wasted time arguing about what things mean. To answer your other questions, consider the simplest, most accessible case: propositional logic. We have ...


12

Your main issue here seems to be that you are wondering how all the following statements: If the Earth is flat, then the Earth exists. If the Earth is flat, then the Earth does not exist. If there is life on Europa, then the Earth exists. could possibly be meaningfully assigned the same truth value in the real world. These are called vacuous ...


12

Disclaimer: I am a formalist. In my opinion, the right lesson is to question the everyday, intuitive notion of truth — i.e. I boldly assert that the everyday, intuitive notion of truth is also just a means of assigning a value to informal statements. We like to think there is some deeper meaning to it, and there might even be such, but in practice, a ...


10

Not really. The statement "$\sf ZFC$ is consistent" can be translated into a statement about the natural numbers in the standard coding way, it's even a $\Pi_1$ statement as far as $\sf PA$ is concerned. Now, if $\sf ZFC$ is truly consistent, then it cannot prove this fact, so this is a true statement which is not provable. But if $\sf ZFC$ is inconsistent, ...


9

Your idea is sound, but the particular formula you propose $$\neg\exists a:\exists a':\exists a'':( ((a\cdot a')=b) \land \neg (a=(a''\cdot SS0) \lor a=S0) )$$ does not quite express it. The problem is that the quantifier for $a''$ has too large scope -- what your formula says is that it will prevent $b$ from being a power of ...


9

The question is which language you want to use to express it. It can be expressed in the language of Peano arithmetic, and hence in other theories that interpret Peano arithmetic, such as ZFC. The key is to use techniques like the ones for Kleene's $T$ predicate to formalize computability in arithmetic. Using these coding techniques, it is ...


8

Pay attention your mixing syntax with semantic. A theory $T$ is $\omega$-inconsistent if exists a formula $P$ in the language of $T$ such that for every standard natural number $n \in \mathbb N$ the $T$ proves the formula $P(n)$ but it also prove the formula $\exists x \neg P(x)$. The point is the you aren't quantifying over the whole universe of ...


8

This is an extension of a comment below Arthur Fischer's answer. For concreteness we will work with the theory PA but in principle any sufficiently strong theory would act the same. Working in PA, or even in the weaker theory PRA, we can formally prove the implication $$ \text{Con}(PA) \to G_{PA} $$ where $G_{PA}$ is the Gödel sentence of PA. This leads to ...


8

As the quotations reveal, there are indeed two different notions here. 1 & 2 belong together. A formal theory $T$ is negation-complete if for any sentence of $T$'s language, either $T$ proves $\varphi$ or $T$ proves $\neg\varphi$ (in symbols, either $T \vdash \varphi$, then $T \vdash \neg\varphi$). 3 & 4 belong together. A logical system (e.g. for ...


8

On (1). In more standard terminology: A formal theory is [negation] complete if for each sentence (closed formula) φ either φ or ¬φ is provable. A logical deductive system is semantically complete if every sentence (closed formula) φ of the system which is a logical truth is provable. Gödel's incompleteness theorem shows that first-order Peano ...


8

From a philosophical point of view this is really a big question to ask! Actually one would need a good notion of all day truth as well as of mathematical truth, to answer this question. What truth in an all-day sense could possibly mean is discussed virtually all the time throughout the history of philosophy, and I will skip this here. The question what ...


8

Yes. If you take out one axiom (the Axiom of Regularity, which roughly disallows sets to be nested inside themselves), then ZFC is perfectly happy with the existence of sets $x$ such that $x = \{x\}$. Such sets $x$ are usually known as Quine atoms. In fact there are many well-known set theories that explicitly allow the existence of Quine atoms, sometimes ...


7

There is indeed a problem to solve here -- and Gödel does solve it, but much later in his 1931 paper than one tends to expect if one approaches it armed with knowledge of modern paraphrases. We're looking at section 2 of Über formal unentscheidbare Sätze. Gödel first [pp. 176-180] describes a formal proof system P for number theory (simplified from ...


7

Nono! If the system is sound and you have a theory $T$, then everything (structure, or whatever the context is that you are talking about) that satisfies $T$ will also satisfy everything that the system can deduce from $T$. But if $T$ itself is inconsistent, there is no structure (or whatever your context is) satisfying $T$. So it is no problem that there ...


7

There might be a bit of a chicken-and-egg happening here. For the common proofs of Gödel's Incompleteness Theorem, we put special priority on the structure $( \mathbb{N} , 0, S, + , \cdot , \mathrm{exp} )$ of elementary arithmetic. If something is true in this structure, then we often refer to that statement as true. Peano Arithmetic is one attempt to ...


7

Certainly if I give you a formal system with an explicit list of axioms, say 42 of them, then it makes sense to say that the system has 42 axioms. It's hard to dispute that. But you make a good observation, that there many equivalent formal systems with all sorts of different numbers of axioms. To be precise, say two formal systems (using the same symbols) ...


6

I can see a brute-force approach to (trying to) prove it. Assume your infinite sequence starts AC. The next term must be A, so ACA. The next term must be B, so ACAB. Now it starts to get tricky. It seems the 5th term can be A or C, but if you use A then there's no valid 6th term, so in fact the 5th term must be C, so ACABC. The 6th term could be A or B, but ...


6

There are a few problems with this scenario: I doubt there will be much acceptance of a new axiom without useful consequences (e.g. Martin's Axiom has wonderful consequences, so it was accepted). So before people will accept this as a new axiom, you would have to show why this will be a fruitful addition to the current set of axioms of mathematics. I am ...


6

You are confusing the object with its various names. As an object, $\frac12=\frac24$. But you can present it differently. More specifically, in order for the numerator function to be well-defined, you need to choose a representation for each rational first. Similarly, $1+1=2$, but the length of these two expressions is different. Names are syntax, ...


6

Example Let $\Gamma$ the set of first-order Peano axioms: no variables free. 1) $\Gamma \vdash \exists x (x = 0)$ --- easily provable 2) $\Gamma, x=0 \vdash x=0$ --- obvious 3) $\Gamma \vdash x=0$ --- from 1) and 2) by $\exists$-elim : wrong ! 4) $\Gamma \vdash \forall x (x=0)$ --- from 3) by $\forall$-intro, 1) $\Gamma, x=0 \vdash x = 0$ 2) $\Gamma,...


6

The categoricity of the second-order Peano axioms simply means (in the context of ZFC set theory) that every model of ZFC contains exactly one thing (up to internal isomorphism) that it thinks is a model of those axioms. However, different models of ZFC can have different $\mathbb N$s. Each model will think its $\mathbb N$ satisfies the second-order Peano ...


5

Building on Gerry Myerson's answer... The set of forbidden subsequences is stable under the substitutions given by the 3-cycle $\tau=(ACB)$. In other words, if $X_1X_2\ldots X_k$ is forbidden, then so is $\tau(X_1)\tau(X_2)\ldots\tau(X_k)$. Hence those 5 remaining cases compress to 1: two of them are in the orbit of the initial sequence $AC$ handled by ...


5

In first order logic the theory $T$ proving $P(0)$, $P(1)$, etc. is not the same as $T$ proving $\forall n P(n)$. You might wish to read about nonstandard models of arithmetic. Consider the theory $T^{*}$ which consists of $T$ together with the infinite collection of statements $0 < c$, $1 < c$, $2 < c$, etc. for every numeral $n$ you can write in ...


5

A memoizing parser for PEGs works in linear time because of two facts: The number of recursive calls that we may need to memoize the result of is linear because it is the product of the input size and the number of nonterminals in the grammar (which for this purpose is considered to be fixed). The result we need to memoize for each call has constant size -- ...


5

The incompleteness theorem, in its usual form, talks about the natural numbers $\mathbb N$ together with some relations such as $\leq$, constants such as $0$ and $1$ and operations $+$ and $\cdot$. To simplify matters, we are ready to add another operation, exponentiation $n^m$. There is an inductive definition of when a sentence $\varphi$ in the ...


5

There is a wide scientific literature about the use of formal systems to describe human behaviour. In most cases, these formalization techniques have been applied to interactive systems, e.g. to understand the causes of human errors in order to predict their occurrence in human reliability analyses, to explore human-automation interaction and identify ...


5

As Noah so kindly mentioned, my work on set-theoretic mereology is exactly about this question. See my recent paper with Makoto Kikuchi: J. D. Hamkins and M. Kikuchi, Set-theoretic mereology, Logic and Logical Philosophy, special issue “Mereology and beyond, part II”, pp. 1-24, 2016. (click through to the arxiv for pdf) Abstract. We consider a set-...


5

An example of an inductive set is the set FOR of all formulas. This is strictly larger than THM in most cases of interest. (I see I've just repeated Daniel Schepler's comment here.) More generally, suppose that not every formula is a theorem, i.e. $\text{THM}\subsetneq\text{FOR}$. Then pick any formula $\varphi\in \text{FOR}\setminus \text{THM}$, and add it ...


Only top voted, non community-wiki answers of a minimum length are eligible