Questions tagged [first-order-logic]

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

Filter by
Sorted by
Tagged with
1 vote
1 answer
32 views

Are these restatements of m-equivalence correct?

I am not sure if these formulations of the $m$-equivalence of two structures $\mathfrak{A}$ and $\mathfrak{B}$ are correct. Two structures $\mathfrak{A}$ and $\mathfrak{B}$ are $m$-equivalent iff for ...
schuelermine's user avatar
0 votes
0 answers
14 views

questions about proving ACF(Algebraically Closed Fields) has quantifier elimination

Hi I am trying to prove that ACF has quantifier elimination. A. Background: It uses the follow theory: First order theory $\mathcal{T}=\left<\mathcal{L}_\mathcal{A},\mathbb{L}_\mathcal{A},T,T^*\...
Shore's user avatar
  • 311
0 votes
0 answers
39 views

What does $\forall x (Triangle(x) \iff \exists y (Square(y) \land AboveOf(x,y)))$ imply?

I'm trying to make a Tarski World for this structure: $$\forall x (Triangle(x) \iff \exists y (Square(y) \land AboveOf(x,y)))$$ I think that it means the following: Element is a triangle if and only ...
Роман Кирьянов's user avatar
2 votes
1 answer
112 views

How can mathematical logic try to model math, when mathematics are used to define mathematical logic?

I've done so far a few courses in logic and formal verification, and I've always wondered: mathematical logic, at least as Hilbert envisioned, tries to model mathematics. Formally define what a "...
sadcat_1's user avatar
  • 227
2 votes
2 answers
136 views

Do we really need the axiom of regularity? [duplicate]

I don't think I could ever say I understand ZFC if I don't get to the bottom of this question. It all started when we had extensionality and comprehension. Then Russell finds a paradox and here comes ...
The curious amateur's user avatar
0 votes
0 answers
53 views

NBG the intersection of a set and a class

In this post I will assume the NBG set theory For all classes $X$ let $M(X)$ mean $(\exists T)(X \in T)$ i.e. $X$ is a set and not a proper class. Prove that $\left\{X \subseteq Y, M(Y) \right\} \...
Shthephathord23's user avatar
0 votes
1 answer
67 views

Question about Finite Model on Robinson Arithmetic

So I was supposed to create a finite model for Robinson Arithmetic in an exam and show that it was a finite model, but I was unable to do so. Would appreciate any help with this problem because I feel ...
John Doe's user avatar
1 vote
3 answers
100 views

Prove that is a tautology without using truth table [closed]

I can't find a proper formula to prove that $$(p\rightarrow q) \rightarrow ((r ∨ p) \rightarrow (r ∨ q)) $$ Is a tautology; considering it's almost exclusively made up of implications. Can somebody ...
Ali Rammal's user avatar
-1 votes
0 answers
39 views

Show that there exists a ternary operator T such that {T} is functionally complete. [closed]

I know that here exists binary operator like that: T(1,1)=0, T(1,0)=1, T(0,1)=1, T(0,0)=1. But how about ternary?
Jan Nowak's user avatar
8 votes
1 answer
212 views

Does independence-friendly logic have a completeness theorem?

It is a well-known (and frankly magical) property that first-order logic is strongly semantically complete (Gödels completeness theorem). Independence-friendly logic is just like first-order logic but ...
Kevin De Keyser's user avatar
1 vote
0 answers
83 views

Which logic is most fundamental? [duplicate]

A couple of my introductory logic books appeal to modal and set-theoretic notions in building up first-order logic. (They explicitly acknowledge these connections and say, for example, that validity ...
inkd's user avatar
  • 47
1 vote
1 answer
126 views

Infinite statements from finite axioms

I want to know if a given finite subset of axioms of PA1 ( 1st order peano arithmetic ) can prove infinite sentences in PA1 such that those proofs need no other axioms except those in the given finite ...
jason's user avatar
  • 1
0 votes
1 answer
96 views

is arithmetic finitely consistent? [duplicate]

Let's take PA1( First order axioms of peano arithmetic ) for example. From godel's 2nd incompleteness theorem, PA1 can't prove its own consistency, more specifically it can't prove that the largest ...
jason's user avatar
  • 1
1 vote
2 answers
53 views

Modern reference on PA degrees?

I'm currently trying to work my way around some papers from Jockush et al, and PA degrees come up frequently. I'd be interested in a modern reference/survey summarizing the main results on the subject,...
Robly18's user avatar
  • 461
-1 votes
2 answers
40 views

Is $\exists x [(P(x) \vee Q(x))\rightarrow R(x)]$ logically equivalent to $\exists x [(P(x) \rightarrow R(x)) \vee (Q(x)\rightarrow R(x))]$?

Is $\exists x [(P(x) \vee Q(x))\rightarrow R(x)]$ logically equivalent to $\exists x [(P(x) \rightarrow R(x)) \vee (Q(x)\rightarrow R(x))]$? What about if I replace $\exists$ with $\forall$?
CroW's user avatar
  • 133
0 votes
0 answers
49 views

Arithmetization of Turing machines

Refer to Turing's 1936 paper, page 248, last paragraph. I present the paragraph in verbatim below : The expression "there is a general process for determining..." has been used throughout ...
Ajax's user avatar
  • 345
1 vote
1 answer
56 views

Defining Church numerals in higher order logic.

I'm looking for some help with Exercise 5.11. in Bacon's A Philosophical Introduction to Higher-Order Logics. Construct an explicit definition of the finite Church numerals, Num$_{\sigma}$, in higher-...
C D's user avatar
  • 23
0 votes
0 answers
43 views

Why in First order logic, Variables mapping is not included in Structure definition [duplicate]

Although the constants are included in Structure definition and Interpretation definition, but Varibles are included only in Interpretation definition, what is the reason for that, is there any error ...
AAA's user avatar
  • 17
1 vote
0 answers
77 views

Proof of Hahn-Banach theorem from Compactness theorem of FOL

Since the Compactness theorem of FOL is equivalent to the ultrafilter Lemma, which implies Hahn-Banach, the implication is clear to me. I was more just wondering if there is a nice direct proof? I saw ...
Niko Gruben's user avatar
0 votes
1 answer
230 views

Precise axiomatic definition for the equality "=" as a binary relation

Question: What is a simple yet precise definition for "=" as a binary relation? My try: I find two definitions for "equality relation" which seems to be contradictory. The first ...
dodo's user avatar
  • 766
9 votes
1 answer
654 views

Finding a property that is true for every left ideal but not for right ideals

I'm trying to find (or prove that it cannot exist) a property that is true for all left ideals of a ring (with unity) but fails for some right ideal. To rephrase this more rigorously: Consider the ...
Eduardo Magalhães's user avatar
1 vote
0 answers
60 views

Subtleties on comprehension sets

I see that a typical definition of the cartesian product $A \times B$ is $\{ x \in \wp\wp A \cup B: \exists a \exists b (a \in A \wedge b \in B \wedge x=(a,b)) \}$. I have come up with an alternative ...
The curious amateur's user avatar
0 votes
1 answer
119 views

How to say in FOL that P(f) is true and everything else with property P is false?

How to say in FOL: "francis" is "Pope" Nothing is identical to "francis" Except for "francis", is false that something is "Pope" The formula should ...
FMG's user avatar
  • 9
0 votes
0 answers
28 views

Composing Substitution Sets in Predicate Calculus

I was reading Artificial Intelligence: Structures and Strategies for Complex Problem Solving by Luger, and composing substitution sets came up. It said this on page 67: "If S and S′ are two ...
user185543's user avatar
0 votes
1 answer
57 views

Understand a proof on Craig's interpolation Theorem

I am reading Hans Halvorson's The Craig Interpolation Theorem. I cannot make the following lines precise: We claim now that there is an isomorphism $j: N\mid_{L_0}\to M\mid_{L_0}$ ... So, putting the ...
Y.X.'s user avatar
  • 3,935
-1 votes
1 answer
177 views

How restricted variables can be introduced in ZF(Zermelo-Fraenkel) set theory? [closed]

In mathematics, all variables are usually restricted - they can take values only from a certain set (for example, real variables). Let us use for restricted variables the notation $x^t$ where $x$ is a ...
Victor M's user avatar
  • 631
2 votes
1 answer
58 views

If the exponential is definable in an expansion of $\mathbb{\overline{R}},$ then it is definable without parameters

Let $\mathcal{R}$ be an expansion of $(\mathbb{R},+,\cdot,-,<,0,1)$, and suppose that the exponential map is definable. I am asked to show that it is definable without parameters using the fact ...
Donnie Darko's user avatar
3 votes
1 answer
54 views

complement of a property in the lambda calculus

I'm trying to demonstrate that the complement of the complement of a property is equal to the property itself using $\lambda$ notation, i.e. if $G=\lambda x(\neg Fx)$ and $R=\lambda x(\neg Gx)$, then ...
saulkripke321's user avatar
0 votes
0 answers
38 views

Understanding quantifier rules in sequent calculus [duplicate]

I am trying to learn sequent calculus for a while and for the life of me, I cannot make sense of the below quantifier rules for sequent calculus: $L$ $R$ $\forall$ $$\Gamma, A[t/x] \vdash \Delta \...
John Davies's user avatar
0 votes
1 answer
73 views

Proof of the deduction theorem in first-order logic

I understand how to proof the deduction theorem $$(D): \Delta,\varphi\vdash\psi\Rightarrow\Delta\vdash\varphi\rightarrow\psi$$ with a set of propositions $\Delta$ and some propositions $\varphi$ and $\...
Josef K.'s user avatar
0 votes
0 answers
29 views

Dependence of Skolem functions on existentially quantified variables

when skolemizing (like here) apparently we only take into account universally quantified variables, for example for the formula$\forall x\, \exists y : D(x,y)$ for some predicate $D$. If we skolemize ...
Targon's user avatar
  • 1,114
0 votes
1 answer
34 views

Is the claim $(f\in P_1\cap P_2)\Rightarrow[(f\in P_3)\Leftrightarrow(f\in P_4)]$ identical to $(f\in P_1\cap P_2\cap P_3)\Leftrightarrow(f\in P_4)$?

Let $A$ and $B$ be arbitrary finite sets, and let $f:A\to B$ be a function with domain $A$ and codomain $B$. I am reading a paper whose main result reads like this: Let the function $f:A\to B$ ...
EoDmnFOr3q's user avatar
  • 1,052
1 vote
0 answers
19 views

Can I use gaifman locality theorem to ground an first order logic formula to a DNF?

Let us say I have a function-free first order logic language. And I can ground it on a domain $\Delta$ of size $n$. Grounding here means that $\forall x \Phi(x)$ translates to $\land_{a\in \Delta}\Phi(...
SagarM's user avatar
  • 1,789
1 vote
0 answers
24 views

Expressivity vs existence of relational structures?

There is a lot of research into understanding expressivity of first-order logic, or formal languages in general. I am particularly interested in expressivity of graph properties. So for e.g. existence ...
SagarM's user avatar
  • 1,789
6 votes
5 answers
1k views

Confusion about Löb's theorem [duplicate]

To quote wikipedia: Löb's theorem states that in any formal system that includes PA, for any formula P, if it is provable in PA that "if P is provable in PA then P is true", then P is ...
G. Bellaard's user avatar
7 votes
2 answers
410 views

Is axiom of replacement nicely stateable in the language of ETCS?

ETCS has a nice category-theoretic formulation: "well-pointed topos with a natural numbers object and axiom of choice." I'm too new to topoi to really understand all of what's going on, but ...
Cobalt _000's user avatar
3 votes
1 answer
95 views

Why does first-order logic lack of a description like the Stone duality?

Stone Duality characterizes Boolean algebras in terms of spaces. I regard this as being done by identifying an algebra with its ``space of models'', and feel like the barrier for a similar thing to be ...
Y.X.'s user avatar
  • 3,935
1 vote
0 answers
44 views

Finding the primitive recursive characterstic function of a set

Context of the problem I think it is important to say that this is how predicate quantification is defined in my textbook: Let $\omega = \mathbb{N} + \{0\}$, $S_i \subseteq \omega, L_i \subseteq \...
lafinur's user avatar
  • 3,162
-1 votes
1 answer
82 views

Is FOL a formal system? [duplicate]

If a formal system consists of a formal language and a deductive system, and that a deductive system consists of inference rules and axioms, then why do we say that FOL is a family of formal systems ...
Nathan Kaufmann's user avatar
0 votes
1 answer
83 views

Some missunderstanging in the NBG set theory

In the set theory of NBG, the class existence theorem says that for all predicative well formed formulas $\varphi$ (wff's in which the variables quantify only over sets) there is a (unique up to ...
Shthephathord23's user avatar
0 votes
1 answer
61 views

Quantifiers and the meaning of the statement

There's two statements: (i) ∃x (PresentKingFrance(x) → Bald(x)); (ii) ∃x (PresentKingFrance(x)) → ∃x (PresentKingFrance(x) ∧ Bald(x)). I'm not an expert in FOL, but I still understand a little bit. A ...
Егор Галыкин's user avatar
0 votes
1 answer
50 views

Resolution Exponential Memory Blowup

I'm looking at the Davis-Putnam algorithm. I don't understand how resolution results in an exponential blowup in the size of the formula, since it seems that after each step, the size is reduced. $(...
David Cheung's user avatar
0 votes
1 answer
54 views

How to show if $\Gamma\models\bot$, then $\Gamma$ is not satisfiable?

I am struggling to show that for any set of sentences $\Gamma$, if $\Gamma\models\bot$, i.e. $\Gamma$ entails $\bot$, then $\Gamma$ is not satisfiable, i.e. for any structure $M$, $M\not\models\Gamma$....
John Davies's user avatar
0 votes
1 answer
25 views

Can a bottom sign be omitted in a disjunction?

I have got the following statement: ∀aP(a),∀a(¬P(a)∨S(a)) ⊢∀a S(a)∨¬P(a) My proof looks like this: ∀aP(a) (premise) ∀a(¬P(a)∨S(a)) (premise) Start scope of x as substitution of a P(x) (forall ...
vMysterion's user avatar
0 votes
1 answer
69 views

Name of Simple Logical System

There's a logical system, devised by someone whose name escapes me, that consists of two moves. You begin with one line, then draw another line, and somehow this can be built to capture all sorts of ...
inkd's user avatar
  • 47
0 votes
1 answer
27 views

Negation for definition of a series frequent in some set

Say a sequence $\left(a_n\right)_{n\in \mathbb{N}}$ is frequent in some set $A$ if $\forall N \in \mathbb{N} : \exists n \ge N : a_n \in A$. Would the negation of this be $\exists N \in \mathbb{N} : \...
Izak's user avatar
  • 167
0 votes
1 answer
107 views

How do "informal" statements in set theory correspond to formal statements in (e.g.) the language of ZFC?

I posted a question on here a few days ago about the formal definition of "well-definedness", but I don't think that question really got at the heart of what I was confused about. Here is an ...
M. Sperling's user avatar
1 vote
1 answer
63 views

Bi-interpretability implies isomorphism of the automorphism groups?

The theorem of Ahlbrandt and Ziegler says that two countable $\omega$-categorical structures $M$ and $N$ are bi-interpretable if and only if $Aut(M)\cong Aut(N)$ as topological groups. Dropping the ...
Focaccia's user avatar
0 votes
1 answer
40 views

Is it decidable whether a classically valid first-order formula is also intuitionistically valid?

Intuitionistic first-order predicate logic is not decidable for arbitrary formulas. However, suppose that we are given a formula of first-order predicate logic that is classically valid. Is there a ...
Adam Dingle's user avatar
2 votes
1 answer
100 views

Translating "nobody likes a sore loser"

I tried translating the utterance "nobody likes a sore loser" into FOL. Using the following glossary, $S(x)$: $x$ is a sore loser $L(x, y)$: $x$ likes $y$ I came up with the following two ...
user51462's user avatar
  • 673

1
2 3 4 5
108