Skip to main content
8 votes

Undecidable predicate logic is decidable by people?

The author is incorrect. A consequence of Godel's incompleteness is that any sufficiently complex logic has statements that are true, but have no proof of truth. If every statement had a proof or ...
Joey Eremondi's user avatar
5 votes
Accepted

Undecidable predicate logic is decidable by people?

Keep in mind that the book was written for undergraduate students, and there are aspects of logic that will demand a considerable level of sophistication, which is often omitted at this introductory ...
André Souza Lemos's user avatar
5 votes
Accepted

Contingent sentences can always be true

In mathematical logic - the discipline of logic that has interested computer scientists the most - there is a difference between proof-theoretic truth and model-theoretic truth. Beyond metaphor (of ...
André Souza Lemos's user avatar
2 votes

Consequences of a language that hides his lower level rappresentations

There's plenty of precedent for this in real programming languages. One obvious example is pointers/references, which are internally just an address (probably). The language/runtime must know this, ...
Pseudonym's user avatar
  • 22.2k
1 vote
Accepted

How can I prove that LTL formula is valid?

There are two main technique in order to prove validity (or more in general, to solve the problem of satisfiability over a definite model) for a LTL formula. The first one is based on semantic tableau,...
user6530's user avatar
  • 954
1 vote

Incomplete definition of function- first order logic

First of all in your above 3 "recursive definitions" linking $\Sigma$ with $\Sigma_2$, clearly the function $g$ in $\Sigma_2$ doesn't have any role in defining the values of $f(t)$ in $\...
cinch's user avatar
  • 235
1 vote

equivalence of validity above different alphabet

You can use $P$ to express $c$ and $R$ to express $f$. The following will guarantee that $P$ is satisfied as a unique element: $$ \exists c \, P(c) \land \forall c_1,c_2 \, (P(c_1) \land P(c_2)) \...
Yuval Filmus's user avatar
1 vote
Accepted

Showing the following sequents are not valid

First, $\phi \models \psi $ means that $\psi$ is a consequence of $\phi$. In other words, if $M$ is a structure and if $M \models \phi$ ($M$ models $\phi$) then $M \models \psi$ ($M$ also models $\psi$...
fade2black's user avatar
  • 9,837
1 vote
Accepted

Verifying execution of code in trustless environment

This is the problem of securely outsourcing computation. There's lots of work on this problem in the cryptographic literature; if you do a search at [Crypto.SE] and [Security.SE], you should find ...
D.W.'s user avatar
  • 161k

Only top scored, non community-wiki answers of a minimum length are eligible