Questions tagged [first-order-logic]
First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.
179
questions
0
votes
1answer
12 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
49 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
46 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
294 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
40 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
16 views
Set of inference and first-order resolution
In Robinson's first-order resolution, we're usually interested in reaching a contradiction $\bot$ from a set of clauses $\Gamma = \{C_1, ..., C_n\}$ where each $C_i$ is a set of first-order atoms. We ...
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
68 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
26 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
35 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
31 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
35 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
25 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
49 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
55 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
27 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
92 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 ...
0
votes
0answers
13 views
Synthesis of the crisp programs from the Bayesian (probabilistic) programs?
https://arxiv.org/abs/2001.00805 is the article which is pointing towards the direction that the optimal policy of the reinforcement learning can be expressed as the Bayesian/probabilistic program (...
0
votes
0answers
29 views
Bounds on the size of the universe of a model for an FO-sentence
Sorry for the weird title.
The Problem:
Consider the first-order logic sentence
φ≡∃s∃t∃u∀v∀w∀x∀yψ(s,t,u,v,w,x,y) where ψ(s,t,u,v,w,x,y,) is a
quantifier-free first-order logic formula using ...
0
votes
0answers
20 views
Can full first order knowledge base be written as the single sequent in the sequent calculus?
The knowledge base of the first order logic essentially is single formula: conjunction of individual formulas (I guess, I am right). The sequent for the sequent calculus is the formula in the special ...
0
votes
0answers
15 views
Is it possible to write down every Prolog program+query as the sequent in the sequent calculus?
Prolog program P is set of Horn (definite) clauses, effectively it is the conjunction of implicational formulas. I guess that every Prolog program P with some query Q can be written as ...
2
votes
0answers
26 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
49 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
55 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 ...
0
votes
0answers
16 views
How to compute (partial) consequence set for premises of the first order logic?
I am playing with the Sequent Calculus Trainer https://www.uni-kassel.de/eecs/fachgebiete/fmv/projects/sequent-calculus-trainer.html . It is game with judgments, where each judgment consists from: 1) ...
2
votes
1answer
42 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 ...
0
votes
1answer
46 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
31 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
161 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
89 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
31 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
38 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
60 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
487 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
59 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
29 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
52 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
44 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
146 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
162 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
42 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
62 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
30 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
38 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
28 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 ...
