48
votes
Accepted
Are there more truths than proofs?
That's correct, but it is not very interesting: we don't have "access" to most mathematical facts. It is not even clear what a proof of an arbitrary mathematical fact would mean, because to ...
42
votes
Accepted
How do we know what natural numbers are?
How do the mathematicians that write standard natural numbers have formal consensus on what they are talking about?
Mathematicians work in a meta-system (which is usually ZFC unless otherwise stated)....
36
votes
Accepted
Do we have to prove how parentheses work in the Peano axioms?
In formal language theory (most relevantly, context-free languages), there is the notion of an abstract syntax tree. A decent chunk of formal language theory is figuring out how to turns flat, linear ...
35
votes
With this definition of completeness, Gödel's Incompleteness result seems not surprising, so why it was back then?
Did people really thought that for every theory and a given formula, either it or its negation are semantically valid, i.e. fulfilled by every model?
(Emphasis added). No, of course not. It's easy to ...
30
votes
Can you give me an example of an implicit use of Godel's Completeness Theorem, say for example in group theory?
A simple example might be something like the following:
Proposition: An element $g \in G$ of a group and any of its conjugates $hgh^{-1} \in G$ have the same order.
This is a collection of first-...
28
votes
How do we know what natural numbers are?
Yes, as you phrased it in a comment:
So even the academic usage of the term standard natural number trusts in our intuitive understanding from preschool?
That's exactly how it is.
We believe, ...
24
votes
Accepted
How to convert numerical claims to first order logic?
Here are some possible ways to make these kinds of numerical claims in general:
'At least n' (Method 1)
"There is at least 1 P" : $\exists x P(x)$
"There are at least 2 P's" : $\exists x \exists y (...
22
votes
Accepted
What exactly is a contradiction and how does it differ from falsity?
Your understanding is correct. Put simply, a contradiction is a sentence that is always false. More precisely,
A statement is a contradiction iff it is false in all interpretations.
In propositional ...
20
votes
Accepted
With this definition of completeness, Gödel's Incompleteness result seems not surprising, so why it was back then?
EDIT: I've added here some of the facts from the discussion between me and the OP in the comments below the question. These doesn't address the actual OP - "why was Godel's theorem surprising?" - but ...
19
votes
Accepted
Convert "Only Believers respect God" to predicate logic.
OP's proposed solution is that there exists at least one believer, who also respects God. This is not equal to the original request, and indeed need not even be true. For example, if nobody ...
19
votes
How to think about theories that prove their own inconsistency?
When we think about theories like ZFC or PA, we often view them foundationally: in particular, we often suppose that they are true. Truth is very strong. Although it's difficult to say exactly what it ...
19
votes
Accepted
What will be the negation of this statement:
Yes, that works.
In logic, the original is:
$\forall x (S(x) \rightarrow \exists y (H(y) \land I(y,x) \land \exists z (P(z) \land L(z,y) \land ((R(x) \land B(x)) \lor (E(x) \land K(x)))))$
If you ...
19
votes
With this definition of completeness, Gödel's Incompleteness result seems not surprising, so why it was back then?
It may be useful to point out that there are (at least) two purposes for which axiomatic theories are created and, as a result, two sorts of theories, for which we may have very different expectations....
19
votes
Accepted
In his 1931 incompleteness proof, how does Godel's definition of "immediate consequence" work?
Welcome to Math.SE!
Maybe every other mode of logical consequence is in some sense equivalent to modus ponens?
Yes, modus ponens is the only propositional inference rule defined in Principia ...
18
votes
Understanding ZFC
ZFC does generate a “theory”. Formally speaking, a theory is simply a set of sentences in the given formal language. Any set of axioms generates a theory, namely the collection of sentences provable ...
18
votes
Accepted
The meaning of an implication with the existential quantifier
Example c was written: $ \exists x (C(x) \to F(x))$
The answer to that example was given as "Someone is a comedian and that means they are funny"
That is an incorrect translation. Imagine a ...
17
votes
Distributive Property of Quantifiers
here are some basic distributive properties in quantifiers, hope it might help someone.
∀x(P(x) ∧ Q(x)) ≡ (∀xP(x) ∧ ∀xQ(x))
∃x(P(x) ∧ Q(x)) → (∃xP(x) ∧ ∃xQ(x))
∀x(P(x) ∨ Q(x)) ← (∀xP(x) ∨ ∀xQ(...
17
votes
Accepted
Second-order logic as the basis for set theory
The thing about the second-order of $\sf ZFC$ is that $M$ is a model of second-order $\sf ZFC$ if and only if $M$ is isomorphic to $V_\kappa$ for an inaccessible $\kappa$. So right off the bat you ...
17
votes
Accepted
Are quantifiers redundant by treating free variables as implicitly universally quantified?
The problem with replacing $\exists$ with $\neg\forall\neg$ to not have to worry about the order of quantifiers becomes apparent if you actually try doing so and omitting the quantifiers. For ...
16
votes
Are these arguments invalid?
A nice tool for analyzing these kinds of categorical syllogisms are Venn Diagrams. Let's do this for the first argument. First, draw a Venn diagram for the 3 sets of things involved in the argument:
...
16
votes
Accepted
Why do first order languages have at most countably many symbols?
You can have as many symbols as you like in your language! For instance, with a possibly uncountable language $L$, the Lowenheim-Skolem theorem becomes:
If $\mathcal{M}$ is an $L$-structure, then ...
16
votes
Set theoretic concepts in first order logic
The questions assumes that there is some notion of "set" in first-order logic itself, but there is not. We use sets to study first-order logic, particularly the semantics (models) aspect. But these ...
16
votes
Why not ban nested quantifiers over the same variable?
It could be done, as described in the other answers.
But it would not make capture-avoiding substitution easier to define, so there's no real benefit.
On the other hand, we would lose the sometimes ...
16
votes
Accepted
How do we compare the set of natural numbers in different models of ZFC
We cannot compare the $\omega$s in different models, can we? If we say that one is embeddable into another, an embedding $\omega\rightarrow\omega'$ between the two sets of natural numbers in different ...
16
votes
Accepted
Nonstandard infinite / hyperfinite sum in IST
Welcome to Math.SE!
You did not indicate how much background you have in Internal Set Theory (IST) - but based on what you wrote, it seem like you have a few misconceptions about it. Let us start by ...
16
votes
Accepted
Confusion about Löb's theorem
Say that the formal system is $\sf PA + \lnot Con(PA).$ Then the system proves every statement is provable in $\sf PA$, but surely it doesn't prove every statement (unless it is inconsistent, which by ...
15
votes
Accepted
Infinitely many axioms of ZFC vs. finitely many axioms of NBG
This is because the framework described by the NBG axioms is strictly richer than that which the ZFC axioms describe. This is not an isolated phenomenon. Let me show you diffrent, perhaps a bit less ...
15
votes
Applications of intuitionistic logic
One fun answer is "programming languages". It turns out a good way to study programming languages is by viewing them as proof systems, and the programming languages you get in this way tend ...
14
votes
Accepted
What is wrong with this naive approach to Hilbert's 10th problem?
The problem is that it's possible $f$ has no integer roots, but there is no proof of this fact (in whatever theory of arithmetic you are using). You're right that if $f$ does have a root, then you ...
Only top scored, non community-wiki answers of a minimum length are eligible
Related Tags
first-order-logic × 12519logic × 6845
quantifiers × 1195
model-theory × 1167
discrete-mathematics × 778
propositional-calculus × 767
logic-translation × 434
set-theory × 367
solution-verification × 338
natural-deduction × 327
elementary-set-theory × 312
proof-writing × 220
formal-proofs × 219
peano-axioms × 168
proof-theory × 149
incompleteness × 128
axioms × 126
notation × 124
proof-explanation × 122
definition × 96
foundations × 91
formal-languages × 84
reference-request × 82
satisfiability × 82
induction × 75