Stack Exchange Network

Stack Exchange network consists of 175 Q&A communities including Stack Overflow, the largest, most trusted online community for developers to learn, share their knowledge, and build their careers.

Visit Stack Exchange

Questions tagged [first-order-logic]

For questions about formal deduction of first-order logic formula or metamathematical properties of first-order logic.

213
votes
2answers
7k views

Is there a 0-1 law for the theory of groups?

For each first order sentence $\phi$ in the language of groups, define : $$p_N(\phi)=\frac{\text{number of nonisomorphic groups $G$ of order} \le N\text{ such that } \phi \text{ is valid in } G}{\...
35
votes
7answers
2k views

**Ended Competition:** What is the shortest proof of $\exists x \forall y (D(x) \to D(y)) $?

The competition has ended 6 june 2014 22:00 GMT The winner is Bryan Well done ! When I was rereading the proof of the drinkers paradox (see Proof of Drinker paradox I realised that $\exists x \...
30
votes
2answers
781 views

Is $ \pi $ definable in $(\Bbb R,0,1,+,×, <,\exp) $?

Is there a first-order formula $\phi(x) $ with exactly one free variable $ x $ in the language of ordered fields together with the unary function symbol $ \exp $ such that in the standard ...
23
votes
3answers
2k views

Axiom of Choice: What exactly is a choice, and when and why is it needed?

I'm having trouble understanding the necessity of the Axiom of Choice. Given a set of non-empty subsets, what is the necessity of a function that picks out one element from each of those subsets? For ...
22
votes
4answers
6k views

What is the purpose of free variables in first order logic?

I understand the difference between free and bound variables, but what are free variables actually useful for? Can't you use quantifiers to express everything that you would want to express with both ...
21
votes
4answers
2k views

How do we know what natural numbers are?

Do I get this right? Gödel's incompleteness theorem applies to first order logic as it applies to second order and any higher order logic. So there is essentially no way pinning down the natural ...
20
votes
2answers
454 views

First order definition of $\pi$

$e$ has a very short first-order definition. It's the only constant that makes this true: $$\forall x,e^x\ge x+1$$ What about $\pi$? What's the shortest first-order definition we could give it? I'm ...
19
votes
5answers
3k views

With this definition of completeness, Gödel's Incompleteness result seems not surprising, so why it was back then?

According to wikipedia a theory (i.e. a set of sentences) is complete iff for every formula either it, or its negation, is provable. On the other side, a logic is complete iff "semantically valid" ...
19
votes
0answers
235 views

Does “every” first-order theory have a finitely axiomatizable conservative extension?

I've now asked this question on mathoverflow here. There's a famous theorem (due to Montague) that states that if $\sf ZFC$ is consistent then it cannot be finitely axiomatized. However $\sf NBG$ ...
18
votes
6answers
2k views

Do we have to prove how parentheses work in the Peano axioms?

One thing that has bothered me so far while learning about the Peano axioms is that the use of parentheses just comes out of nowhere and we automatically assume they are true in how they work. For ...
18
votes
4answers
3k views

How does Gödel Completeness fail in second-order logic?

So a while ago I saw a proof of the Completeness Theorem, and the hard part of it (all logically valid formulae have a proof) went thusly: Take a theory $K$ as your base theory. Suppose $\varphi$ ...
18
votes
4answers
1k views

Is the negation of a non-theorem a theorem?

I don't know if that is something obvious or if it is a dumb question. But it seems to be true. Consider the non-theorem $\forall x. x < 1$. Its negation is $\exists x. x \geq 1$ and is a theorem. ...
18
votes
1answer
634 views

Is $\Bbb R$ definable in $(\Bbb C,0,1,+,*,\exp)$?

Is there a first-order formula ϕ(x) with exactly one free variable $x$ in the language of fields together with the unary function symbol $\exp$ such that in the standard interpretation of this ...
17
votes
3answers
11k views

Predicate vs function [duplicate]

In logic, what is the difference between a predicate and a function? To be specific, I am just interested in First Order Logic. Thanks!
16
votes
3answers
1k views

Why does what I've written fail to define truth?

I stumbled across a set of axioms for first order logic a bit ago. Intrigued, I decided to try to write it all down and organise what I read. After I did that, it seemed to me as though one could ...
15
votes
3answers
2k views

Is the compactness theorem (from mathematical logic) equivalent to the Axiom of Choice?

Or more importantly, is it independent of the axiom of choice. The compactness theorem states the given a set of sentences $T$ in a first order Language $L, T$ has a model iff every finite subset of $...
15
votes
2answers
858 views

Gödel's completeness theorem and the undecidability of first-order logic

I'm working through this module, "Undecidability of First-Order Logic" and would love to talk about the two exercises given immediately after the statement of Godel's completeness theorem. First, ...
14
votes
2answers
2k views

How to find the shortest proof of a provable theorem?

Roughly speaking, there are some fundamental theorems in mathematics which have several proofs (e.g. Fundamental Theorem of Algebra), some short and some long. It is always an interesting question ...
14
votes
5answers
2k views

categorical interpretation of quantification

Many constructions in intuitionistic and classical logic have relatively simple counterparts in category theory. For instance, conjunctions, disjunctions, and conditionals have analogues in products, ...
14
votes
5answers
2k views

What will be the negation of this statement:

Every street in the city has at least one house in which we can I find a person who is rich and beautiful or highly educated and kind. Negation: 'There exists a street in the city where in every ...
14
votes
1answer
657 views

Can all math results be formalized and checked by a computer?

Can all math results, that have been correctly proven so far, be formalized and checked by a computer? If so, what type of logic would need to be used there? I've heard that the first-order logic is ...
14
votes
1answer
575 views

A *finite* first order theory whose finite models are exactly the $\Bbb F_p$?

Since this question turned out to be trivial, I'm now asking this strengthened version: Is there a finitely axiomatized first order theory $T$ in the language of rings such that its finite models ...
13
votes
5answers
2k views

Most astonishing applications of compactness theorem outside logic

The compactness theorem has a lot of applications to logic and model theory. I'm looking for applications. I'm looking for theorems in other areas of mathematics which seem at first sight to have ...
12
votes
2answers
915 views

How to prove that Gödel's Incompleteness Theorems apply to ZFC?

Let us denote Robinson Arithmetic as Q and Primitive Recursive Arithmetic as PRA. Let $T$ be a formal theory formulated in the language of arithmetic. According to this page on the Stanford ...
12
votes
0answers
678 views

Why can't we formalize the lambda calculus in first order logic?

I'm reading through Hindley and Seldin's book about the lambda calculus and combinatory logic. In the book, the authors express that, though combinatory logic can be expressed as an equational theory ...
11
votes
2answers
1k views

Why do first order languages have at most countably many symbols?

Every proof that I read seems to assume that $|L|\leq\aleph_0$. But then how do you model things like field over $\mathbb{R}$ without running out of variable symbols? More importantly, how can I ...
11
votes
2answers
507 views

How to think about theories that prove their own inconsistency?

There are consistent first-order theories that prove their own inconsistency. For example, construct one like this: Assuming their is a consistent and sufficiently expressive first-order theory at ...
11
votes
3answers
1k views

Are the natural numbers implicit in the construction of first-order logic? If so, why is this acceptable?

I have recently been reading about first-order logic and set theory. I have seen standard set theory axioms (say ZFC) formally constructed in first-order logic, where first-order logic is used as an ...
11
votes
1answer
786 views

What is wrong with this naive approach to Hilbert's 10th problem?

Background: I have been studying some decidability results in number theory. In doing so, I have always assumed there was no need for me to study pedantic definitions of decidability using Turing ...
11
votes
1answer
824 views

First Order Logic: Prove that the infinitely many twin primes conjecture is equivalent to existence of infinite primes

I'm learning First Order Logic independently using a college textbook. I've been doing some self exercise question in it and came across this one, which I can't seem to figure out how to do: Let ...
11
votes
2answers
12k views

Online tools for checking validity of classical, intuitionistic, … logic formulas?

What online tools are available, where one can enter a formula of (first order) propositional or predicate logic, and have it check whether it is valid classically, intuitionistically, or even ...
11
votes
2answers
2k views

Relationship between propositional logic, first-order logic, second-order logic higher-order logic, and type theory

I understand there is propositional logic, first-order logic, second-order logic higher-order logic, and type theory, where the latter logics are extensions of the former logics. Can someone explain ...
10
votes
4answers
588 views

What's the point of allowing only quantification of variables in first-order logic.

In first-order languages, ${\forall}$ is allowed to quantify only over variables, so that ${\forall}v(P)$, where $v$ is some variable and $P$ is a WFF is the only kind of a WFF concering universal ...
10
votes
4answers
182 views

Problems teaching introductory logic. Is this a statement? “If x is an integer, then…”

Consider the claim, "If $x$ is an integer, then $x^3>0$". Is this a statement? My text defines a statement as "a declarative sentence which is true or false, but not both." At first it seemed ...
10
votes
4answers
478 views

Why ZFC+FOL cannot uniquely describe/characterize R or N?

I find the following text on the Wikipedia page on first order logic: "First-order logic is the standard for the formalization of mathematics into axioms and is studied in the foundations of ...
10
votes
1answer
568 views

On proving the zero-one-law for first order logic

I'm trying to understand the proof of the zero-one-law for first order logic as provided in (Ebbinghaus-Flum, 1995). It goes as follows: Let $\tau$ be a relational signature. Let $r\in\mathbb{N}$, ...
9
votes
1answer
983 views

Why isn't there a first-order theory of well order?

Problem 1.4.1 of Model Theory by Chang and Keisler asks, Is there a theory of well order in the first-order language $\{\leq\}$? I'm pretty sure the answer is no, since well order is a property of ...
9
votes
2answers
1k views

Is there a Second-Order Axiomatization of ZF(C) which is categorical?

A theory $T$ is called categorical if it only has one model upto isomorphism. (Note: this has nothing to do with category theory.) The Lowenheim-Skolem theorem states that no first-order theory with ...
9
votes
2answers
314 views

Advantages of finite axiomatizability

I've seen it written in a number of places that one of the "advantages" of NBG over ZFC is that it is finitely axiomatizable. I was wondering, what are some examples of how this is advantageous? I ...
9
votes
1answer
150 views

Is the following theory consistent?

Suppose, we have a first-order logic theory over a signature {=, $\times$} (where $\times$ is a binary function symbol, and = is the equality symbol), that contains following axioms: $$\forall x \...
9
votes
1answer
429 views

Defining new symbols (abbreviations) in first-order logic

In first order logic it is common (and just about necessary) to introduce new symbols which have been defined in terms of the "fundamental" symbols of a given theory. For instance, the signature of ...
9
votes
1answer
448 views

Infinitely many axioms of ZFC vs. finitely many axioms of NBG

It is known that ZFC needs infinitely many axioms, but NBG (Neuman-Bernays-Gödel set theory) is finitely axiomatizable (as first-order theories of course). But both theories agree completely on the ...
8
votes
7answers
696 views

What happens if the empty set is not a subset of every set? [duplicate]

$\hskip8pt$ Definition. If $A$ and $B$ are sets, then $A$ is a subset of $B$ iff every element of $A$ is also an element of $B$. The empty set $\{\}$ is a subset of every set because, if $A$ is an ...
8
votes
3answers
677 views

Why does Skolemming not preserve validity?

I'm wondering what exactly is meant when people say "Skolemization preserves satisfiability but not validity". I'm having trouble wrapping my brain around it because I think of Skolemization, when ...
8
votes
3answers
201 views

Where are the model theory concepts from?

Look at the following definition. Definition. Let $\kappa$ be an infinite cardinal. A theory $T$ is called $\kappa$-stable if for all model $M\models T$ and all $A\subset M$ with $|A|\leq \kappa$ we ...
8
votes
2answers
744 views

Are these formal formulas equivalent?

My textbook gave the following $ \forall x_0 (\exists x_1 \ x_0=(\mathbf{O''} \cdot x_1) \vee \exists x_1 \ x_0=((\mathbf{O''} \cdot x_1)+\mathbf{O'})) $, then commented on the syntax and why the ...
8
votes
4answers
579 views

Is the set of PA theorems the same as the set of solvable halting problems?

I am not sure if this is a trivial question. By Post's theorem we know that every PA (first order logic) theorem is equivalent to stating that a given input C in a given Turing machine halts or doesn'...
8
votes
1answer
840 views

Uncountable Dense Linear Orders

Is there an example of two uncountable equipollent dense linear orders without endpoints that don't satisfy the same first order properties? Or is it true that two uncountable equipollent dense linear ...
8
votes
1answer
3k views

What is the operator precedence for quantifiers?

Is the term $$\forall x p(x) \rightarrow \forall x q(x)$$ equal to $$\forall x (p(x) \rightarrow \forall x q(x))$$ or $$(\forall x p(x)) \rightarrow (\forall x q(x))$$ In other words: What is the ...
8
votes
1answer
133 views

Semantic proofs to syntactic proofs

Given a first-order logic theory $T$ and and a formula $F$, suppose I have semantically proved that $T\vdash F$. That is, I have proved that any model $M$ of $T$ satisfies $F$ and I conclude by Gödel'...