Questions tagged [first-order-logic]
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.
221
questions
1
vote
0
answers
20
views
How do I prove relations of two CTL formulas?
If I have two CTL equations, how do I prove they're equivalent or that one implies the other?
What's the general approach? Disproving is obvious, but I am unable to figure out how to prove the ...
- 121
3
votes
1
answer
167
views
how to do incremental construction of the minimal model in logic programming?
I was reading a book titled "Essentials of Logic Programming.", most parts of the book are easy to understand. but now having a problem with Theme 45: incremental constructions of the ...
- 984
0
votes
1
answer
51
views
Is any 2-CNF has 2-DNF representation?
I was asked a question whether I could come up with a 2-CNF over several variables that has no 2-DNF representation. However I thought that any CNF can be converted to DNF through some manipulations e....
- 103
0
votes
0
answers
16
views
Is first order linear temporal logic a special case of first order modal logic?
Propositional linear temporal logic is a special case of propositional modal logic. Is first order linear temporal logic likewise a special case of first order modal logic?
- 237
0
votes
2
answers
144
views
Can you help me in finding an algorithm that finds the first unique number in an array with lowest position?
I have the following problem to solve:
Given a non-empty array A consisting of N integers, the task is to find the first unique number in the array. A unique number is defined as a number that occurs ...
2
votes
2
answers
68
views
'Someone' in first order logic
I have in the lectures a sentence in English, which I have to translate to First Order Logic.
Someone who loves all animals loves all humans.
Textbook solution:
∀x.(is_human(x) ⇒ is_animal (x))
⇒
∀...
- 23
0
votes
0
answers
41
views
Minimum DNF length of a conjuction of equivalences
Show that the formula $\bigcap_{i=1}^n (X_i \leftrightarrow Y_i)$ cannot have an equivalent disjunctive normal form with less than $2^n$ clauses.
I am puzzled on what approach to take -- whether to ...
- 109
1
vote
0
answers
43
views
Understanding unprovable halting, model theory, and (in)completeness
I know computability, but not model theory and logic, so this question may be naive or confused in that respect.
A blog post of Scott Aaronson mentions a Turing Machine $M^*$ such that the statement P:...
- 4,099
0
votes
1
answer
40
views
How substituituion composition is associative?
I'm not convinced that substitutions are associative, I read the https://en.wikipedia.org/wiki/Substitution_(logic)#First-order_logic and the https://www.youtube.com/watch?v=_cVNeccMF-E
My problem is ...
- 243
1
vote
1
answer
50
views
Substitutions unions vs composition are not the same?
I'm studying substitutions. A substitution is a set of mappings from variables to terms $\{a \rightarrow b; c \rightarrow d;...\}$.
Given these substitutions:
$\sigma_1 := \{x \rightarrow y\}$
$\...
- 243
1
vote
1
answer
69
views
Simple Skolemization Question
Is it correct that, under a certain signature S, two First Order Logic formulae F and G are equisatisfiable if (F is satisfiable under S iff G is satisfiable under S)? But in Skolemization I’m ...
0
votes
0
answers
51
views
First-Order logic exercise
I'm trying to solve the following exercise:
Given this is true:
\begin{align} \neg \forall x \space \ \exists y \ ( x\neq y \rightarrow LeftOf(x,y) )\end{align}
Demonstrate :
\begin{align} \exists y \...
- 1
0
votes
1
answer
484
views
Finding the loop invariant for Array Reversal
I've been assigned to find the loop invariant for the following code:
...
- 103
1
vote
1
answer
42
views
What does :: indicate in all-quantifier predicates?
Can somebody explain to me the meaning of $::$ in the following predicate?
$$(\forall i : P(i) : Q(i)) \equiv (\forall i :: P(i) \implies Q(i))$$
- 121
1
vote
2
answers
196
views
Logical consequence problem, doubt
It is possible to have this logical consequence?
$$
\forall x (p(x) \vee q(x)) \models \forall x p(x) \vee \forall x q(x)
$$
- 13
1
vote
1
answer
53
views
Why we can't use deduction theorem on soundness to contravene second incompleteness with lob's theorem
I'm starting to learn modal logic and there is something that's bothering my mind for a while.
we know from deduction theorem that $((\vdash q) \rightarrow (\vdash p)) \Leftrightarrow(\vdash (q \...
2
votes
1
answer
37
views
First-order model checking is not fixed parameter tractable on general graphs
I read that the problem of first-order model checking is believed to be not fixed parameter tractable on general graphs.
Why is this the case? Would be happy about some reference
Thanks in advance!
- 35
1
vote
0
answers
24
views
Prove that any first-order logics with equality and a relation/functional symbol of arity more than 1 is undecidable
Definition: A formal logic system is decidable – if there is an algorithm that can determine if any given sentence is a theorem (or not).
Based on this definition, I am not sure how to move to prove ...
- 493
-1
votes
2
answers
85
views
Is there a quantifier more powerful than the other to determine FOL connector?
So basically we have 2 types of quantifier in first order logic, they are universal quantifier and existential quantifier. Usually we use implies connector(->) when we have universal quantifier in ...
0
votes
0
answers
22
views
How can I prove KB╞ α?
Is correct to use ~α as rule to prove KB╞ α?
Is possible to unify sentence ~V(x,y) v S(x) with V(N,W)?
...
- 1
1
vote
1
answer
34
views
First-order iteration operator example
I am reading on https://en.wikipedia.org/wiki/FO_(complexity)#Iterating that FO[$t(n)$] consists in first-order logic with an iteration operator that iterates $t(n)$ number of times some quantifier ...
- 407
-1
votes
1
answer
65
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 ...
2
votes
1
answer
76
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 ...
- 143
0
votes
0
answers
40
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. ...
- 1
3
votes
1
answer
74
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 ...
- 448
0
votes
0
answers
34
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 ...
- 113
1
vote
1
answer
50
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 ...
- 183
0
votes
1
answer
63
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 $\...
- 113
1
vote
0
answers
91
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 ...
- 113
6
votes
4
answers
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 ...
- 183
0
votes
1
answer
91
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 ...
- 463
3
votes
1
answer
102
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 ...
- 463
1
vote
1
answer
98
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 ...
- 99
2
votes
2
answers
114
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 ...
- 99
2
votes
1
answer
82
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 ...
- 99
2
votes
1
answer
28
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)...
- 99
1
vote
1
answer
74
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|=\...
- 99
1
vote
1
answer
41
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 ...
- 99
1
vote
1
answer
99
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 ...
- 310
0
votes
1
answer
88
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: ...
- 27
0
votes
1
answer
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 ...
- 301
0
votes
0
answers
44
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 ...
- 131
1
vote
0
answers
19
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 ...
- 448
1
vote
0
answers
45
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 ...
- 679
1
vote
0
answers
23
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 $...
- 448
4
votes
0
answers
54
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,...
- 485
1
vote
0
answers
45
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
0
answers
52
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).
...
- 407
0
votes
1
answer
55
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-...
- 155
2
votes
1
answer
35
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 ...
- 123