2022 Developer Survey is open! Take survey.

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
0 answers
8 views

Is it possible to define logspace reductions with FO[TC] queries?

Assume that we have a NP problem A, and a NP-complete problem B under logspace reductions. Furthermore, lets assume that we encode the problem A into a relational database $D_A$, and B into another ...
user avatar
1 vote
1 answer
35 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))$$
user avatar
  • 115
1 vote
2 answers
189 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) $$
user avatar
  • 13
1 vote
1 answer
39 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 \...
user avatar
2 votes
1 answer
21 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!
user avatar
0 votes
0 answers
20 views

Creating a new list with with every other element

I am new to Isabelle, I am looking for a way to extract every other element of a list into a new list. Similarly, how do I extend it to extracting every 3rd element of a list? For example, given [1,2,...
user avatar
  • 1
1 vote
0 answers
22 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 ...
user avatar
  • 459
0 votes
2 answers
64 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 ...
user avatar
0 votes
0 answers
13 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)? ...
user avatar
1 vote
1 answer
27 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 ...
user avatar
-1 votes
1 answer
26 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 ...
user avatar
0 votes
0 answers
12 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 ...
user avatar
  • 163
2 votes
1 answer
41 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 ...
user avatar
0 votes
0 answers
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 ...
user avatar
0 votes
0 answers
35 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. ...
user avatar
  • 1
3 votes
1 answer
47 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 ...
user avatar
  • 386
0 votes
0 answers
29 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 ...
user avatar
  • 113
1 vote
1 answer
41 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 ...
user avatar
0 votes
1 answer
52 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 $\...
user avatar
  • 113
1 vote
0 answers
47 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 ...
user avatar
  • 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 ...
user avatar
0 votes
1 answer
88 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 ...
user avatar
  • 169
3 votes
1 answer
69 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 ...
user avatar
  • 169
0 votes
0 answers
12 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 ...
user avatar
  • 171
1 vote
1 answer
93 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 ...
user avatar
  • 99
2 votes
2 answers
108 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 ...
user avatar
  • 99
2 votes
1 answer
75 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 ...
user avatar
  • 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)...
user avatar
  • 99
1 vote
1 answer
65 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|=\...
user avatar
  • 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 ...
user avatar
  • 99
1 vote
1 answer
88 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 ...
user avatar
0 votes
1 answer
58 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: ...
user avatar
  • 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 ...
user avatar
  • 279
0 votes
0 answers
29 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 ...
user avatar
  • 131
1 vote
0 answers
15 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 ...
user avatar
  • 386
1 vote
0 answers
36 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 ...
user avatar
1 vote
0 answers
18 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 $...
user avatar
  • 386
4 votes
0 answers
49 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,...
user avatar
  • 445
1 vote
0 answers
41 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 ...
user avatar
1 vote
0 answers
27 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). ...
user avatar
0 votes
1 answer
43 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-...
user avatar
  • 135
2 votes
1 answer
32 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 ...
user avatar
  • 123
0 votes
1 answer
51 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 ...
user avatar
3 votes
1 answer
89 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 ...
user avatar
1 vote
0 answers
51 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 ...
user avatar
  • 1,351
3 votes
1 answer
324 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 ...
user avatar
  • 1,351
0 votes
1 answer
53 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 ...
user avatar
3 votes
1 answer
93 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(,)$}...
user avatar
  • 10.7k
0 votes
0 answers
118 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$ ...
user avatar
  • 23
2 votes
1 answer
63 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 ...
user avatar
  • 23

1
2 3 4 5