Questions tagged [first-order-logic]
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.
229
questions
0
votes
1
answer
29
views
confusion due to the difference of "terms" between FOL and SMT-LIB
In first-order logic (FOL), terms evaluate to values other than truth values, i.e., values of terms are neither true nor false.
Reference: Chap. 2.1 from The Calculus of Computation
By constrast, in ...
- 1
0
votes
0
answers
18
views
How to enumerate theories logically equivalent to natural deduction?
Natural deduction seems to generally be structured around the idea of (an/) introduction and elimination rules(s) for each logical symbol.
I heard that that was an attempt to capture the way humans ...
- 140
4
votes
1
answer
42
views
What is the corresponding lambda-calculus / proof terms of intuitionistic first order logic? (looking for references)
It is an oft-repeated result that lambda calculi correspond to logics. In particular, recall the following (approximate) relationships
intuitionistic propositional logic ⇄ simply typed lambda ...
- 143
1
vote
1
answer
26
views
Is stable infinity required of theories combined with model-based theory combination?
In the paper "Model-Based Theory Combination" (1) by De Moura and Bjorner they present an alternative to the Nelson-Oppen method for theory combination. They first describe the Nelson-Oppen ...
- 163
1
vote
2
answers
43
views
Do stably-infinite theories exclude finite sorts?
Nelson-Oppen requires theories to be stably infinite. Meaning, that each theory allows extending models to have an infinite domain. A commonly mentioned counter example is that the theory of bit ...
- 163
0
votes
0
answers
14
views
Question about PNF equivalency in sub-models
I'm given this formula: $\forall x(\forall zR(x,z)\rightarrow\exists yR(y,x))$.
Now, the statement that this formula is not logically true in every sub-model of a model that makes it logically true, ...
1
vote
1
answer
133
views
Resolution on weakening rule by derived clause
How to prove that every clause that is implied by the input formula (learned or not) can be derived using resolution with weakening rule:
$\frac{C}
{C \vee D}$
(A clause $C$ is implied by $F$ if for ...
- 542
4
votes
0
answers
72
views
Extending Fagin's Theorem to the Polynomial Hierarchy
Fagin's Theorem (see Wikipedia and these lecture notes) states that there is an equivalence between second-order logic (SOL) formulas with existential quantifiers, and problems in NP.
I was wondering ...
- 41
0
votes
0
answers
6
views
Datalog+- doubt about semantics and complexity
I am reading about Datalog+- (e,g, https://ieeexplore.ieee.org/abstract/document/5571709), and I have a doubt about its semantics, and about the complexity of query answering.
In Datalog+-, you write ...
- 499
1
vote
0
answers
39
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 ...
- 324
3
votes
1
answer
172
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 ...
- 1,024
0
votes
1
answer
139
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
2
answers
166
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 ...
3
votes
2
answers
115
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))
⇒
∀...
- 33
0
votes
0
answers
53
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
91
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,179
0
votes
1
answer
59
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
58
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
80
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
52
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
725
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
43
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))$$
- 123
1
vote
2
answers
198
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
61
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
41
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
25
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 ...
- 515
-1
votes
2
answers
88
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
31
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
35
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 ...
- 499
-1
votes
1
answer
74
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
152
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
4
votes
1
answer
94
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 ...
- 548
0
votes
0
answers
39
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
52
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
69
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
100
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
93
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 ...
- 543
3
votes
1
answer
111
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 ...
- 543
1
vote
1
answer
100
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 ...
- 109
2
votes
2
answers
118
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 ...
- 109
3
votes
1
answer
86
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 ...
- 109
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)...
- 109
1
vote
1
answer
85
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|=\...
- 109
1
vote
1
answer
42
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 ...
- 109
1
vote
1
answer
102
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
93
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
24
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 ...
- 321
0
votes
0
answers
48
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 ...
- 141