Questions tagged [first-order-logic]
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.
179
questions
5
votes
0answers
33 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
34 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
12 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
35 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-...
0
votes
0answers
18 views
Is Inductive Logic Programming approach applicable to general theories (not just sets of Horn clauses)?
Inductive Logic Programming (https://en.wikipedia.org/wiki/Inductive_logic_programming) find hypothesis theory H for background theory B and set of examples E. ILP algorithms and implementations ...
2
votes
1answer
25 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
38 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
58 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
47 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
307 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
47 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 ...
0
votes
0answers
28 views
Situation calculus: how to find pre-conditions in 15-puzzle game?
I have been working on finding the preconditions for a situation calculus example for some time now. This example is called the game "15-puzzle" where you can find a discription here https://...
2
votes
1answer
73 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
30 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
37 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 ...
1
vote
1answer
40 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
65 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 ...
0
votes
0answers
34 views
Abstract syntax tree: expression->operation->lhs|rhs vs expression->lhs|operation|rhs - what should I take into account in decision?
I am trying to build class hierarchy for the abstract syntax tree of First Order Logic as specified in the grammar https://github.com/antlr/grammars-v4/blob/master/fol/fol.g4 (ANTLR parser generator).
...
2
votes
1answer
32 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
64 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
65 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
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 ...
1
vote
0answers
110 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
28 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
52 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 ...
0
votes
0answers
29 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"...
3
votes
1answer
75 views
Combining Predicate Logic and BigO
I am a beginner to predicate logic and BigO and am having though time understanding the definition of BigO in terms of predicate logic in the picture attached. I particularly am unable to understand ...
2
votes
1answer
45 views
On satisfiability for 2-variable FOL being NEXPTIME-complete
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 ...
-2
votes
2answers
71 views
How to correctly negate a predicate bounded by some quantifiers?
this is a problem which was asked in GATE CS 2010.
This is question statement:
Q: Suppose the predicate F(x, y, t) is used to represent the statement that person x can fool person y at time t. which ...
0
votes
0answers
35 views
How do you derive a type $∃e(e)$ in terms of universally quantified types, without invoking Void initially?
I wrote a "proof" for this, and though it was enough to convince myself, there are a few things that bother me about it. Primarily I'm not sure about the loose way in which I'm swapping between first-...
0
votes
1answer
32 views
What can't guarded fragment of FO express?
I have some basic confusions about the definition of the guarded fragment of first-order logic. Hopefully someone can tell me where I'm wrong.
GF in FO is defined by:
Atomic formulas, $x=y$ and $R(...
1
vote
3answers
165 views
Can undecidability theorems be detected by a machine? [closed]
this question was originally written in mathoverflow, but a comment recommended me to rewrite it as a CS question.
This is not a mathematically formalized question. I'm sorry for that but think it's ...
1
vote
1answer
104 views
Algorithm for automatic construction of natural deduction proofs
I was wondering if there exists any algorithm for automatic construction of nautral deduction proofs. I'm interested in propositional logic and first order logic.
If there is no algoritm, can you ...
1
vote
1answer
32 views
Logical characterization of $NC^1$
Morioka in his 2005 dissertation [1] referenced "On Uniformity within $NC^1$" by
Barrington, Immerman, and Straubing. Using the following statement:
Every $\mathbf{NC^1}$-predicate is computed by ...
1
vote
0answers
53 views
How can I compute the most general unifier for these two expressions?
I have the following first order logic expressions:
$f(g(a, h(b)), g(x, y)),~f(g(z,y), g(y, y))$
and I want to compute the most general unifier for them. If I follow the algorithm found on these ...
1
vote
1answer
67 views
MSO (Monadic second-order logic) Logic On Words
Let L be a language over $\Sigma = \{a,b,c\}$ that contains all words, where the length $|w|_b$ (number of all b's) has remainder 1 if divided by 3.
MSO logic over words are definded as follow:
I ...
0
votes
2answers
588 views
The barbers paradox first order logic formalization
I tried to look on the site and while I found some similar questions, I did not find the first order logic formalization of the following sentence (the basic barber's paradox), so I wanted to ask if I ...
3
votes
1answer
61 views
Basic second-order logic example contains a mistake?
I'm reading the following course on second-order logic, by Péter Mekis :
http://phil.elte.hu/mekis/sol.pdf .
The course seems excellent, but I'm stuck on one of his first examples for showing the ...
1
vote
1answer
30 views
List of all possible reasoning tasks - satisfiability and theorem proving only?
What is the exhaustive list of reasoning tasks? As far as I can understand, then any logical reasoning reduces to 2 tasks only: 1) satisfiability problem (finding the assignment of the variables) and ...
5
votes
2answers
2k views
Why do ¬, ∀ and ∃ have the same precedence?
I thought the order of precedence of operators and quantifiers was arbitrary, but I don't really understand why those three have the same "strength" in relation to other operators (e.g., ¬ will have ...
2
votes
0answers
54 views
Ontology Editor or Something Else (in my case)? [closed]
Does there exist a system, e.g., software, an environment, a programming language, or the like, to represent knowledge and to reason with it, to query with, where the (descriptive) language used is at ...
2
votes
1answer
46 views
Terminology First-Order Logic
A graph $G$ is said to be a model of a first-order sentence $\varphi$ if $G$ satisfies $\varphi$. Now let $\varphi(x_1,...,x_r)$ be a first order formula with free variables $x_1,...,x_r$. What is ...
2
votes
0answers
45 views
Reference Request - Typed First-Order-Logic Book
There are many great references for computer scientists interested in untyped first order logic, such as Melvin Fitting's "First-Order Logic and Automated Theorem Proving" or John Harrison's "Handbook ...
0
votes
1answer
161 views
Is it possible to encode logical expression and interpret it with SQL?
Is it possible without any forms of eval or stored procedures to execute a query, which interprets logical expression, encoded in some way in a table (or two tables)...
2
votes
1answer
163 views
Decidability of equivalence to existential formulas
I'm looking for an algorithm to decide if a given first order formula over a fixed vocabulary admits a logically equivalent existential one (i.e. a formula in prenex form where all quantifiers are ...
3
votes
1answer
44 views
Refutation in first order logic
Consider the following statement
In FOL, we can reduce entailment checking to satisfiability checking:
$S \models S' \iff S \land \neg S'$ is satisfiable (This proof
strategy is called ...
2
votes
0answers
64 views
What is the computational complexity of the first-order theory of real arithmetic?
Tarski proved that the first-order theory of real-closed fields is decidable. Is the exact computational complexity known? The best upper bound I could find is EXPSPACE [1], where it is also ...
2
votes
0answers
31 views
Superposition calculus: greater vs greater-or-equal
Bachmair and Ganzinger 1991, 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', specifies the criterion for using an equation as, by some appropriate ordering, ...
1
vote
1answer
40 views
Superposition calculus: Elimination of redundant atoms
Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', section 5.2, 'Simplification and Deletion Techniques', page 17, 'Elimination of redundant ...
1
vote
1answer
29 views
Bachmair and Ganzinger, ordering of equations
Bachmair and Ganzinger (1991), 'Rewrite-Based Equational Theorem Proving With Selection and Simplification', page 4, defines an order on equations. (This is an arcane piece of machinery but a critical ...
