# Questions tagged [first-order-logic]

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

4,703 questions
Filter by
Sorted by
Tagged with
1 vote
10 views

16 views

### Least Herbrand Model with Fixed Point Semantics

Not really sure if this is the appropriate forum for this question as a code snippet is involved. I came across the following Prolog program : ...
43 views

1 vote
66 views

### Proof Verification: Effectiveness of Tarski-Vaught Test

Here is the definition of the Tarski-Vaught test from Marker's Model Theory: An Introduction page 44. Proposition 2.3.5 (Tarski-Vaught Test) Suppose that $M$ is a substructure of $N$, then $M$ is an ...
1 vote
41 views

### How to show that the Alexander Subbase Theorem is ZF-equivalent to the Compactness Theorem for first order logic?

Alexander Subbase Theorem (ASB): Let $X$ be a topological space. $X$ is compact if and only if there is a subbase $\mathcal{B}$ for the topology of $X$ such that every subcollection of $\mathcal{B}$ ...
40 views

### Quantifiers and usage of the infinum

Let $A$ be a set. Define $d(x,A) = \inf \{d(x,a)| a \in A \}$. So for any $a$, $d(x,A)\leq d(x,a)$ and for any other $r \leq d(x,a)$ we have $r \leq d(x,A)$. Now let $x$ and $y$ be two different ...
16 views

### Show that the set {a ∈ R | a > 0} is definable in LRng = {+, ·, 0, 1} [closed]

Let L := LRng = {+, ·, 0, 1} be the language of ring theory, where 0 and 1 are constant symbols and + and · are binary function symbols, and let M be an L-structure such that |M| = R, 0M = 0 ∈ R, 1M = ...
1 vote
57 views

24 views

More formally, what I want to find is a set $A \subset \mathbb{N}$ s.t. for every formula $\phi$ with only one free variable $x$ in Peano arithmetic, there exists $a \in A$ s.t. $\{ x \mapsto a \} \... -1 votes 1 answer 36 views ### Why for a zeroth-order logic is not possible to have a complete Peano arithmetic with quantifier free arithmetical sentences? In my previously question I still have some doubts and in particular about this part Peano arithmetic is impossible to rewrite into zero-order logic since Peano arithmetic has functions like the ... -1 votes 1 answer 61 views ### First Order Logic Question: How to interpret ∀x~∃y when L(x,y) means ___x loves ___y? [closed] I am given a sentence and my professor wishes for me to convert it to FOL. The problem is that I do not know what the form of this quantifier order would look like. For instance, if L(x,y) means ___x ... 1 vote 0 answers 41 views ### Proofs that monadic second order logic is not compact I was reading this comment by Simone on this answer to this question. The comment is reproduced below, emphasis mine. Well, It's not an extension that uses the notation you use, but all axioms remain ... 0 votes 1 answer 46 views ### Does Every Axiom Set For Classical Propositional Calculus Have Two Negations, and If So, Why? Every axiom set for classical propositional calculus (under uniform substitution and detachment) with a conditional and negation connective that I've seen has at least two negation symbols in it (and ... 0 votes 1 answer 67 views ### Is this theory trying to capture the theory of the minimal model of ZFC correctly formalized? I'm trying to capture theory$T_0$written by Noah's answer to a prior posting of mine. First we add a constant symbol$\mathcal M$to the language of set theory. Now we add all axioms of$\sf ID$and ... 0 votes 0 answers 81 views ### In which way is possible to rewrite signature of Peano arithmetic in a zero-order logic? For example in second-order logic, it is possible to define the addition and multiplication operations from the successor operation, but this cannot be done in the more restrictive setting of first-... 0 votes 0 answers 34 views ### can I falsify a traditional inference with modern natural deduction like system? I can represent a traditional syllogism with the language of first-order predicate logic. and If the syllogism is valid, then I can prove it with natural deduction system or tableaux. If the syllogism ... 0 votes 1 answer 48 views ### Give a deduction showing that ∃x∀yRxy syntactically implies ∀y∃xRxy I know it's true but I have no idea how to write the deduction as there is no ∃ elimination rule that I know of. Am I supposed to use some kind of substitution? 0 votes 0 answers 68 views ### Proposition 3.23 of Logic for Mathematicians by A.G. Hamiltom? Just case 3. I am trying to understand the proposition 3.23 of Logic for Mathematicians by A.G. Hamiltom. But I am confused by the proof of case 3. Please help me. Let$\mathscr A(x_i)$be a wf. of$\mathscr L$... 1 vote 2 answers 80 views ### In proof by induction, is it more correct to say "we use induction on n" or "we use induction on the set of natural numbers"? When proof by induction is started, it is common to see a statement of the form "we use induction on _". For example, say we were trying to prove $$\forall n (n \in \mathbb{N} \implies \sum\... 3 votes 2 answers 81 views ### A property of L-structures related to model completeness Let T be a an L-theory & suppose \mathcal{A} is a structure satisfying all existential consequences of T. I want to show that there is a model \mathcal{M}⊨T embedding in an elementary ... 0 votes 1 answer 54 views ### Is there a minimal constructible model for every first order theory that has some? If a first order theory T has a constructible model, then does that entail that T must have a minimal constructible model, i.e. one that is homomorphic to every constructible model of T. By &... 0 votes 0 answers 20 views ### Mapping binary relation to first order logic I am self-learning my way through this topic and appreciate help with red marked questions. For (c), I am stuck in thinking, if nothing is mapped to nothing, what is it? Potentially empty? But (h) I ... 1 vote 1 answer 45 views ### A language \mathcal{L} with n atomic propositions can express 2^{2^n} non-equivalent propositions I tried to prove the statement and wasn't sure if it is correct. Theorem A language \mathcal{L} with n atomic propositions can express 2^{2^n} non-equivalent propositions. Proof Two propositions ... 0 votes 1 answer 32 views ### Completeness of a theory that is not \omega-categorical Let T be the theory of linear orders with no endpoints and let \mathcal{L}=\{<,c_0,c_1,\dots\} be the language that consists of a binary relation symbol and a countable amount of constant ... 0 votes 0 answers 27 views ### What is incorrect with my first-order predicate calculus? I'm trying to write the FOL for "Borrowing a book doesn’t change who owns it" given the functions: Book(x) = x is a book Owns(x, y) = x owns y Provide(x, y) = x provides y My attempt was ∀... 2 votes 0 answers 41 views ### Question about \omega-categoricity Let T be the theory of linear dense orders with no endpoints and let \mathcal{L}=\{<,c_0,c_1,\dots\} be the language that consists of a binary relation symbol and a countable amount of constant ... 1 vote 1 answer 36 views ### Does swapping the quantifiers change meaning for the following case? [duplicate] Case 1: \exists x\forall y\;.\; P(x,y) Case 2: \forall x\exists y\;.\; P(x,y) I have tried to write them and convince myself of an answer: Case 1: There exists an x for every y such that P(x,... 4 votes 1 answer 69 views ### Elementary equivalence of ordinals as ordered sets I am trying to solve this problem: Show that \aleph_1 and \omega are not elementarily equivalent as ordered sets (here \aleph_1 denotes the first uncountable cardinal) Show there exists some ... 4 votes 1 answer 50 views ### \forall\exists-sentence true in all finite fields is true in algebraically closed fields? Let \phi be a \forall\exists-sentence in the language of rings that is true in every finite field. I want to show that \phi is true in every algebraically closed field. I know that ACF is ... 4 votes 1 answer 96 views ### Is proving metatheorems circular logic? [duplicate] I am currently learning mathematical logic, and I came across a dilemma. In proving metatheorems (theorems about formal systems), almost all the proofs for said metatheorems used mathematics (... 1 vote 2 answers 94 views ### How to tell when mathematical objects are of different types, e.g. 1 and 0.5, or 1 and +\infty. I heard that for the purposes of doing set theory, we adopt the convention that the statement x=y is automatically false if x, y are of different types; for instance, if one is treating sets and ... 0 votes 1 answer 10 views ### Can First-Order Horn formulae contain existential quantifiers? I am trying to understand which formulas are encapsulated by first-order Horn logic, with an aim of differentiating it from other logics used for knowledge representation and reasoning (KRR). My ... 0 votes 2 answers 37 views ### What is the difference between using a conjunction and implication with existential quantifiers? When using existential quantifiers, is there a difference between using a conjunction and implication? For example, for this question: There is an agent who sells policies only to people who are not ... 0 votes 2 answers 60 views ### FOL for “x and y have exactly two common neighbors.” Let E be a binary relation symbol representing adjacency in graphs. (That is,$$E(x, y) means in a graph that “the vertices$x$and$y$are adjacent”.) Write a formula$\phi(x, y)$in the first-... 1 vote 0 answers 68 views ### Has this logic of relations been done before? First Order Logic of Relations "FOLR": Language: first order logic with Equality "$=$"(and its axioms), and Membership "$ \in $", nLinks "$\overrightarrow {x_1,..,...
30 views

Are smt-solvers (like z3) theoretically able to (always correctly) check consistency of any 1.-order logic formula? How does smt-solver algorithm work in details? Are there any algorithms that could ...
27 views

### Rewrite proposition with logical symbols

I want to rewrite the following proposition in mathematical language (and by mathematical language I mean symbols such as: $\forall , \exists, (, ), \implies$ and so on). Proposition: Every non-...
37 views

### How to justify the use of witnesses with arguments in proofs in ZFC

When dealing with $\varepsilon,\delta$ statements, we often choose an arbitrary $\varepsilon\gt0$, and let $\delta\gt0$ be chosen to satisfy some $\varphi(\varepsilon,\delta)$, and then continue our ...
36 views

55 views

### Check a proof using structural induction of a formula constructed from a grammar

I have built a proof for the folowing statement. However I am not sure if it is correct... Could you please help me assert if it is correct? Edit I have made my proof based on the exercise 14 of the ...
32 views

### Proof of Completeness Theorem in Enderton's Logic, satisfiability of Γ∪Θ∪Λ

I have similar question with this post Proof of Completeness Theorem in Enderton's Logic, satisfiability of Γ∪Θ∪Λ, so I quote some of his/her description: I'm reading the proof of the Completeness ...