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

• 101
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 : ...
• 320
43 views

• 125
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 ...
• 6,569
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}$ ...
• 2,982
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 ...
• 493
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

• 2,982
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 \} \... • 433 -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 ... • 127 -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 ... • 6,569 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 ... • 10.7k 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 ... • 3,553 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-... • 127 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 ... • 67 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? • 11 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\... • 1,725 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 &... • 3,553 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 ... • 185 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 ... • 57 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,... • 177 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 ... • 199 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 ... • 199 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 ... • 11 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 ... • 121 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-... • 13 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,..,...
• 3,553
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 ...
• 111
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-...
• 887
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

• 939
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 ...
• 17
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 ...
• 1
35 views

How to build a proof using structural induction? [duplicate]

I am requested to build a proof for the following I am requested to prove the following statement, however I have no idea on how to begin... Does any of you know how can I do such induction on the ...
• 17