Questions tagged [first-order-logic]
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.
204
questions
-1
votes
1answer
19 views
Conjuctive Normal Form
Let f(P,Q,R) be the truth-function defined as follows. f(P,Q,R)=1 if and only if
Q and R have different truth-values; or
P and R have the same truth-values.
Choose all formulas that are in conjunctive ...
0
votes
0answers
10 views
What could be a good reference for types and tables in First Order Logic?
My research caters mostly to Statistical Relational Learning community, so Probability + Logic. I would like to provide a reference for the concept of types and tables in First-Order Logic, as ...
2
votes
1answer
34 views
Resolution algorithm does not seem to generate the empty clause
Let's assume I have the following 3 clauses:
$\neg T$,$\neg Q$, ($\neg P \lor Q \lor S \lor T)$,$(\neg U, T, \neg S)$,$(\neg U, T, P)$
and I want to see if our KB entails $\neg U$ so I tried to apply ...
0
votes
0answers
10 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
30 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
39 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
38 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
48 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
41 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
87 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
66 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
9 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
89 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
56 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
85 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
23 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
24 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
34 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
59 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
47 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
20 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
49 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
82 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
48 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
89 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
98 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
55 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
240 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
129 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
29 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
147 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
68 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 ...
