# Questions tagged [first-order-logic]

First-order logic is a formal logical system used in mathematics, philosophy, linguistics, and computer science.

153 questions
Filter by
Sorted by
Tagged with
1answer
221 views

### Using existential quantifier within implication

I had used an existential quantifier within an implication, as below: $$\exists ~ \sigma_{opt}~~~ \wedge~~~ n \in R^{+}~ ,~0<n<1 \rightarrow ~~ \sigma_{opt} = n$$ I've, recently, found that ...
1answer
61 views

### Is this formula valid?

is this formula valid ??, if it is not what interpretation could i use ? (∀ x: P(x) -> ∀ x: Q(x)) -> ∀ x: (P(x) -> Q(x)). PS : i know that the other implication is valid.
1answer
528 views

### Quantified Boolean Formula vs First-order logic

Is Quantified Boolean Formula (QBF) the same as First-order logic (FOL)?
2answers
621 views

### Why is first-order logic (without arithmetic) VALIDITY only recursively enumerable, and not recursive?

Papadimitriou's "Computational Complexity" states that VALIDITY, the problem of deciding whether a first-order logic (without arithmetic) formula is valid, is recursively enumerable. This follows from ...
2answers
2k views

### Predicate Logic Notation: What does a “dot” mean?

What does a dot (.) mean in predicates? $\forall a \in A. \exists d \in D. H(a,d)$ Especially, how is the above different to $\exists d \in D. \forall a \in A. H(a,d)$ I've never seen this used ...
3answers
1k views

### What is the relation between First Order Logic and First Order Theory?

I thought that any FOT is a subset of FOL, but that does not seem to be the case, because FOL is complete (every formula is either valid or invalid), while some FOT (like linear integer arithmetic) is ...
2answers
1k views

1answer
3k views

### Horn clause to Prolog [closed]

At the needs of my HW at uni I need to transform some Horn clauses to Prolog but I cannot figure out how to do it. I found out some guides but they describe how to do it with only one fact. So can you ...
1answer
299 views

### Why ⊢ for affirmative predicates and ⊨ for ¬negations?

I read a book which says that in Predicate Calculus, syntactic theorem proving is identical (complete and sound) with semantic entailment and this is very useful because it is easier to prove positive ...
1answer
211 views

### Logic Question - Why is This an Implication?

I have a question about predicate logic. Suppose we have the following predicates: $\text{Study}(x,y)$: x studies y $\text{Comp}(x)$: x is a computing student I want to encode the following ...
4answers
294 views

### No number is equal to Zero, is this statement true or false?

While reading an article on logic, there is a sentence "No number is equal to zero" and we have to assign truth values to this sentence. I hope this is true and the article says it as false. Can ...
0answers
154 views

### On the Turing Completeness of First Order Logic

It is well known that in Descriptive Complexity Theory FO is equivalent to AC0. However, this accepts a couple of a theory and a string <T,s> iff the ...
1answer
179 views

1answer
596 views

### first order logic resolution unification

Assuming I have shown part of the knowledge base in the clausal format:  p1(banana).  not p1(X) or p2(Y).  p1(X) or not p3(F). ... and more rules. ...
1answer
858 views

### Difference between intended interpretation and extended interpretation in first-order logic

I am currently reading "Artificial Intelligence - A modern approach" and I really do not get the difference between intended interpretation and extended interpretation in first-order logic. Are ...
1answer
563 views

### MGU and Variable Standardization - CNF

I have been reading on converting first order logic sentences to conjunctive normal form, and then performing resolution. One of the steps of converting to CNF, is to Standardize variables: rename ...