We are building EduLadder(ELADR) - Protocol

The Eladr Protocol is a decentralized, security and efficiency enhanced Web3 noSQL database powered by IPFS as the data storage layer https://ipfs.io/, and the Cardano block chain as the rewards token platform, https://cardano.org/. It provides a JSON based, IPFS layer 2 solution for data indexing and retrieval in an 'append only' file system built with open source Node.js API libraries.

The ELADR token was designed to incentivize and reward community members as a proof of contribution. Token holders are also granted access to EduLadder.com premium features as well as associated ELADR token enabled apps.

WHITE PAPER Buy Now Try BETA

Real Problems! Real Experts!

Join Our Telegram Channel !


The Eduladder is a community of students, teachers, and programmers. We help you to solve your academic and programming questions fast.
In eduladder you can Ask,Answer,Listen,Earn and Download Questions and Question papers.
Watch related videos of your favorite subject.
Connect with students from different parts of the world.
Apply or Post Jobs, Courses ,Internships and Volunteering opportunity. For FREE
See Our team
Wondering how we keep quality?
Got unsolved questions? Ask Questions

Digital-circuit-and-logic-design-->View question

What is undecidability of predicate logic?

in terms of logic of computers


Asked On2017-06-07 06:26:09 by:milan-ransingh

Taged users:
Nikhil-bharadwaj

Likes:
Be first to like this question

Dislikes:
Be first to dislike this question
Talk about this  Like  Dislike
View all questions
Answers

Theorem: It is undecidable whether a first order logic formula is provable (or true under all possible interpretations).

Proof: Suppose there is an algorithm B that, given a first order logic and a formula in that logic, decides whether that formula is valid (holds under all possible interpretations). I will use that to give a decision algorithm for the language {(M,w) | M is the description of a Turing machine that accepts the string w}. As the latter problem is undecidable this will show that B cannot exists.

Given M and w, create a first order logic by declaring a constant eps, a unary function symbol a for every letter a in the alphabet, and a binary predicate fq for every state q of M.

Consider the following interpretation of this logic: Variables x range over strings over the given alphabet, eps denotes the empty string, a(w) denotes the string aw, and fq(x,y) indicates that M, when given input w, can reach a configuration with state q, in which xy is on the tape, with x in reverse order, and the head of M points at the first position of y. Under this interpretation fq0(eps,w) is certainly a true formula, as the initial configuration is surely reachable. Here q0 is the initial state, and w is a representation of w made from the constant and function symbols of the logic. Furthermore the formula there exists there exists y: fq-acc(x,y) with q-acc the acceptance state, holds iff M accepts w.

Whenever M has a transition from state q to state r, reading a, writing b, and moving right, the formula

for all for all y: fq(x,ay) => fr(bx,y)

holds. Here x and y are variables. Likewise, if M has a transition from state q to state r, reading a, writing b, and moving left, the formulas

for all for all y: fq(cx,ay) => fr(x,cby)

hold for every choice of a letter c. In addition we have

for all for all y: fq(eps,ay) => fr(eps,by),

covering the case that M cannot move left, because its head is already in the left-most position. Finally, there are variants of the formulas above for the case that a is the blank symbol and that square of the tape is visited for the first time:

for all for all y: fq(x,eps) => fr(bx,eps
for all for all y: fq(cx,eps) => fr(x,cbeps
for all for all y: fq(eps,eps) => fr(eps,beps).

Let T be the conjunction of all implication formulas mentioned above. As M has finitely many transitions and the alphabet is finite, this conjunction is finite as well, and thus a formula of first order logic. Now consider the formula

fq0(eps,w) & T => there exists there exists y: fq-acc(x,y).

In case M accepts w, there is a valid computation leading to an accept state. Each step therein corresponds with a substitution instance of one of the conjuncts in T, and using the laws of first order logic it is easy to check that the formula above is provable and thus true under all interpretations. If, on the other hand, the formula above is true under all interpretations, it is surely true in the given interpretation, which implies that M has an accepting computation starting on w.

Thus, in order to decide whether or not M accepts w, it suffices to check whether or not the formula above is 


Answerd on:2017-06-08 Answerd By:prajwalamv

Likes:
Be first to like this answer

Dislikes:
Be first to dislike this answer
Talk about this  Like  Dislike

Type your answer here in no less than 50 words :



Lets together make the web is a better place

We made eduladder by keeping the ideology of building a supermarket of all the educational material available under one roof. We are doing it with the help of individual contributors like you, interns and employees. So the resources you are looking for can be easily available and accessible also with the freedom of remix reuse and reshare our content under the terms of creative commons license with attribution required close.

You can also contribute to our vision of "Helping student to pass any exams" with these.
Answer a question: You can answer the questions not yet answered in eduladder.How to answer a question
Career: Work or do your internship with us.Work with us
Create a video: You can teach anything and everything each video should be less than five minutes should cover the idea less than five min.How to upload a video on eduladder