Questions tagged [first-order-logic]

First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.

Filter by
Sorted by
Tagged with
0
votes
0answers
9 views

Convert referent of an sentence into an if statement

I was reading Deductive logic in Natural Language.It said that meaning of sentence depends on meaning of words. My question is that can this technique be used along with set theory to convert the ...
0
votes
0answers
28 views

Why is “For all the simple things you have done to me, there exists one thing that makes me happy” FALSE? Use nested quantifiers to prove your point

I've done my due dilligence and tried to answer this question using every resource I could get. KhanAcademy, NesoAcademy, and Rosen's Discrete Mathematics book. I still can't wrap my head around it. ...
2
votes
1answer
38 views

Uses of of the one-variable fragment of first-order logic aka S5

I'm looking at decidable fragments of first-order logic. It seems that FO(1), i.e. the one-variable fragment of first-order logic is equivalent to the modal logic S5. However, I cannot find a ...
0
votes
0answers
26 views

Specific quantifier elimination for real algebraic numbers

It is well-known that the theory of (first-order) real arithmetic, $\mathcal{T}_{\mathbb{R}}$, is decidable, both on its linear and non-linear (a.k.a field) fragments, since Tarski-Seindenberg proved ...
1
vote
1answer
36 views

Restriction in description logic

$Human ⊓ ¬Female ⊓ (∃married.Doctor) ⊓ (∀hasChild.(Doctor ⊔ Professor))$ Here, $∃married.Doctor$ means if there exists an individual who is married to Bob belongs to $Doctor$ concept. But my ...
0
votes
1answer
47 views

Domain of discourse vs First-order theory

In the question (Validity of predicate logic formulas) I see the following way of expressing: "The predicate $P(x,y) \equiv \bigl[ y \cdot x = 1 \bigr]$, where the domain of discourse is $\...
1
vote
0answers
39 views

SMT validity solvers/ quantifier elimination in Ocaml

I am working on my own expression package in Ocaml and have to perform both validity queries and quantifier elimination. I have already implemented Cooper's procedure (for Presburger and Linear ...
6
votes
4answers
4k views

How is ‘x + ½ = 2 and x ∈ ℤ’ an open statement?

I was watching this video on statements. There is an example: $x + \frac12 = 2$ It's an open statement as the truth value could be T or ...
0
votes
1answer
86 views

Mechanically proving element non-membership

I'm facing a (possibly simple) problem while proving a theorem. I need to show that under several (true) assumptions, some element is not in a set. Such assumptions are all met and there is are ...
3
votes
1answer
63 views

PetersonNP, mechanical mutual exclusion proof

Good day everyone, I'm currently trying to carry out the PetersonNP (a.k.a. FilterLock) correctness proof (mutual exclusion). I've found several proof sketches on concurrency books but I'm interested ...
0
votes
0answers
8 views

An efficient algorithm for determining unifiable pairs

The first order resolution rule is given as: $$\frac{P\lor L_1 \qquad \neg Q \lor L_2}{L_1 \sigma \lor L_2\sigma}$$ where $\sigma$ is the most general unifier of $P$ and $Q$. Therefore, one is asked ...
1
vote
1answer
88 views

Incomplete definition of function- first order logic

Let $\Sigma=\{c,f^1,R_1^2,...,R_k^2\}$ where $c$ is constant, $f$ is one argument function, and $R_i$ are binary relations. Let $\Sigma_2=\{c',g^2,R_1'^1,...,R_k'^1\}$ where $c'$ is constant, $g$ is ...
2
votes
2answers
105 views

Problem with formalism in first order logic

This is a general question in first order logic. Assume I have alphabet $\Sigma$ that contains one-argument function (among other symbols). I want a new alphabet, $\Sigma'$, which is the same as the ...
2
votes
1answer
71 views

equivalence of validity above different alphabet

Given the next alphabets: $\,\,\Sigma_1=\{R^2,P^1,=^2\}\,\,,\Sigma_2=\{c,f^1,=^2\}.$ Prove of Disprove: There's exists an algorithm, that given formula $A$ above $\Sigma_2$, builds formula $A'$ above ...
2
votes
1answer
27 views

non-existence of sentence that captured specific property

For a sentence $\varphi$, we'll define $Spec(\varphi)$ to be the set of all $n\in\mathbb{N}$ for which there is a model $M$ with $|D^M|=n$, such that $M\models\varphi$. Let $\Sigma=\{P(\cdot),R(\cdot)...
1
vote
1answer
55 views

First-order logic - Does there exist a sentence that is satisfiable by all infinite models and only by them?

Prove or Disprove: There is $\boldsymbol{no}$ alphabet $\Sigma$ and closed formula (no free variables) $\varphi$ above $\Sigma$, such that for any Model $M$ it holds that $M\models\varphi\iff\,|D^M|=\...
1
vote
1answer
39 views

Validity of formulas in very specific alphabet

Let $\Sigma = \{c_1, c_2, R(\cdot,\cdot) \}$ be an alphabet in first-order logic without $=$, where $c_1,$ $c_2$ are constant variables and $R$ is binary relation. Let $\varphi$ be a formula without ...
1
vote
1answer
82 views

There is an $n^k$ prover if and only if $P = NP$

I am studying computational complexity using Papadimitrious's book: "Computational Complexity". I am trying to solve the final statement of Problem 8.4.9, but I am stuck and would like some ...
0
votes
1answer
52 views

Tuple relational calculus: existential quantifiers

I have the following question and given answer: Question: List the names of managers who have at least one dependant. Answer: ...
0
votes
1answer
22 views

Partitions of star-free languages and questions on the proof of the Splitting Lemma by Diekert/Gastin

I'm currently reading a paper on First-order definable languages by Volker Diekert and Paul Gastin. Im having trouble understanding a part of the proof for lemma 3.2 (splitting lemma). The part I'm ...
0
votes
0answers
23 views

Practical ml model explainability with graphs and prolog

How practical are logic engines for proof paths combined with knowledge graphs in Providing reasonable explainability for ML models trained using GNNs? Adding more context. there is a history of ...
1
vote
0answers
14 views

Good exposition of tableau for first-order logic with equality?

I'm looking for a resource (online or printed) that explains in a self-contained way the classic tableau for first-order logic with equality. All I can find are expositions of tableaux for first-order ...
1
vote
0answers
32 views

Multiple parameter predicates and the Relational Model

I've got a very general question about the relational model and it's relationship to 1st order predicate calculus. It will probably seem very basic to most, I'm afraid, a consequence of me grappling ...
0
votes
0answers
53 views

A necessary condition for a relation to be in 2NF but not in 3NF is that some non-prime attribute must be determined by a non-prime attribute

I will state the complete question now, since it did not fit in the title. Is the statement given below correct? A necessary condition for a relation to be in 2NF but not in 3NF is that some non-...
1
vote
0answers
17 views

Modal logic equivalent to two-variable first-order logic?

It is well-known that many modal logics can be viewed as fragments of $FO^2$, i.e. two-variable first-order logic. But is there a modal logic that is not a fragment, but is expressively equivalent to $...
4
votes
0answers
45 views

Do FOL theorem provers accept axiom schemata?

Axiom schemata (such as ZFC) are, in a sense, infinite sets of axioms. Do the ATPs designed to work with FOL (such as Vampire) accept axiom schemata? I looked in the Vampire "manual" briefly,...
1
vote
0answers
38 views

Help me understand whether these critical pairs are joinable

I have the following TRS $R$: $$ l_1 = f(g(x)) \to f(x) = r_1 \\ l_2 = g(f(y)) \to g(y) = r_2 $$ I want to know if $R$ is confluent, and whether $g(f(f(x))) \leftrightarrow_R^* g(g(g(x)))$. I have ...
1
vote
0answers
19 views

What is the space-complexity of a boolean first-order query?

I have the intuitition that, if we implement a (space-efficient) boolean first-order query solver, the amount of consumed memory should depend on the data size (i.e., it should not be constant). ...
0
votes
1answer
40 views

Functional Abbreviation for Inst Expression in Turing's 1936 Paper

In Turing's 1936 paper On Computable Numbers Page 30-31, and its Correction Page 1-2 : For a Turing Machine $M$, $Inst(q_i S_j S_k L q_l ) $ means that if $M$ scans symbol $S_j $ under $m-...
2
votes
1answer
30 views

first order logic to normal form order of operations

∃y∀x [A(x) ∧ B(y) -> C(x,y)] ∃y∀x [¬(A(x) ∧ B(y)) v C(x,y)] ∃y∀x [¬A(x) v ¬B(y) v C(x,y)] I need to convert the above to conjunctive normal form. I'm a ...
0
votes
1answer
48 views

Does FOL extended with least-fixed points satisfy the Compactness Theorem?

I am aware that first-order logics (FOL) satisfies the compactness theorem. That is, if a FOL theory is insatisfiable, a finite subset of the axioms of such theory is insatisfiable too. Is it the case ...
3
votes
1answer
81 views

How to describe Deterministic Transitive Closure in FOL?

In "Finite Model Theory and Its Applications", page 152, it is said that Deterministic Transitive Closure, on ordered finite structures, captures LOGSPACE. Hence, taking into account that ...
1
vote
0answers
49 views

How to write "∀x.F(x)" for "F(x)=λx.Φ(x)" in one expression (sequel from question about "∀(λφ. (φ x m→ φ y))"?

This question is sequel from How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"? which further explains the notation and context. So - I have anonymous Boolean-valued ...
2
votes
1answer
317 views

How to understand quantifier without predication " ∀(λφ. (φ x m→ φ y))"?

I am reading about embedding/automation of modal logics in classical higher order logic (http://page.mi.fu-berlin.de/cbenzmueller/papers/C46.pdf) and Goedels proof of God's existence is prominent ...
0
votes
1answer
47 views

Consistent theory based on L and not(A->A) is a theorem

I am working on this problem in which I have a theory $T$ based on language $\mathcal{L}$ and the only information we have is that T is consistent and $\vdash \lnot(A \rightarrow A)$. Given this ...
3
votes
1answer
88 views

Expressing functions using the arithmetic dictionary

i have seen in the "logic to cs" class i take - a theorem that states: "every recursive (computable) function $f$ can be expressed using the arithmetic dictionary {$C_0, C_1, f_+(,), f_x(,), R_\le(,)$}...
0
votes
0answers
90 views

Show that exist a finite set of clauses F in first-order logic that Res*(F) is infinite

I'm kind of desperate at this point about this question. A predicate-logic resolution derivation of a clause $C$ from a set of clauses $F$ is a sequence of clauses $C_1,\dots,C_m$, with $C_m = C$ ...
2
votes
1answer
50 views

Unification Algorithm without Occur Check

I have been reading about Unification algorithm here https://en.wikipedia.org/wiki/Unification_(computer_science)#A_unification_algorithm . And I wonder about the importance of occur check. I know ...
0
votes
1answer
59 views

Z-Specification = Routes

Im trying to make an invariant for this Z schema about routes. 1) The invariant should express that each route should contain at least 20 different places. First of all i thought of doing a universal ...
2
votes
1answer
218 views

Natural deduction: understanding bottom elimination (¬e)

I am new to natural deduction and upon reading about various methods online, I came across the rule of bottom-elimination in the following example. I do not understand the step in line 10. Upon ...
2
votes
1answer
34 views

Why is the satisfiability of ESO formulas not equal to the satisfiability of FO formulas?

Existential second-order logic (ESO) formulas have the form $$\Phi = \exists R_1 ... \exists R_k. \phi$$ where $R_1...R_k$ are relation symbols and $\phi$ is a FO formula, which can use the relation ...
2
votes
1answer
120 views

Natural deduction proof: distributivity of existential quantification

In a current exam-prep exercise, we were tasked to prove the following formula using natural deduction of first-order logic: $(\exists x. P \lor Q) \rightarrow P \lor (\exists x.Q)$ for arbitrary $P,...
2
votes
0answers
67 views

Sample applications based on First Order Logic

I often hear about benefits of FOL, but I wonder what are some of its real world applications? Could someone please provide samples/case studies of applications of FOL that address real world ...
1
vote
1answer
28 views

In first order logic, how do we normally represent a statement?

I wanted for an example such as: Everyone has a mother. I've seen that it is represented in FOL as: $\forall x \exists y:$ Mother(x, y) I'm seeing that as:For every x, there exists a y, such that y ...
1
vote
0answers
142 views

Proving a first order logic theorem in equational logic with a term rewriting system

I am trying to translate and prove a theorem, originally written in first order logic (FOL), into a combination of equational logic (EL) and Boolean logic (BL) (more precisely a model of Boolean ...
2
votes
0answers
29 views

How to prove following two statements are equivalent in Hilbert System?

statement 1: $Γ$ is satisfiable implies $Γ$ is consistent. statement 2: If $Γ$ derives $α$ then $Γ$ entails $α$. I can easily prove statement 1 from 2 , but not 2 from 1 (without using strong ...
1
vote
1answer
63 views

General resolution in first order logic

Assuming you have a formula in first order logic like $$(\forall_x p(x) \land \forall_x q(x)) \rightarrow \forall_x(p(x) \land q(x))$$ (which seems valid?) Converting the formula to ...
0
votes
0answers
31 views

Is FOL representation of probabilistic assignment statement correct?

For instance, $x = x + 1[0.3]x+2$ sets $x$ to $x + 1$ with probability $0.3$ and to $x+2$ with probability $0.7$. If I use notation used in the paper "An Analysis of First-Order Logics of Probability"...
3
votes
1answer
116 views

Combining Predicate Logic and BigO

I am a beginner to predicate logic and BigO and am having though time understanding the definition of BigO in terms of predicate logic in the picture attached. I particularly am unable to understand ...
2
votes
1answer
49 views

On satisfiability for 2-variable FOL being NEXPTIME-complete

Let $\mathbf{FO^2}$ be the fragment of first-order logic consisting of sentences with at most two variables and no function symbols. It is well known that satisfiability for $\mathbf{FO}^2$ is ...

1
2 3 4 5