# Questions tagged [first-order-logic]

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

201 questions
Filter by
Sorted by
Tagged with
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 ...
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. ...
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 ...
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 ...
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 ...
47 views

55 views

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,...
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 ...
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). ...
40 views

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 ...
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 ...
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 ...
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 ...
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 ...
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"...
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 ...