I would like to translate a philosophy text into logic axioms and propositions. Then, I would like to use prolog to check if the text is logically consistent.
However, I find it difficult to translate philosophy books into logic. Is there any philosophy book written mainly using logic statements?
Prolog doesn't check the consistency of programs. Doing so would be equivalent to solving the (provably unsolvable) halting problem. In fact, in Prolog, there is no way to assert a negative proposition. At most, you can assert that some proposition is true only if some other proposition is not provable. This is similar to negation in some ways and if you happen to ask the right question (which is not just "is this consistent?") you might get a warning of inconsistency, but it is a long way from a full consistency check on an argument.
But are you sure the property you are interested in is consistency rather than validity? Consistency is a property of theories (a Prolog program is essentially a theory); validity is a property of arguments (the execution trace of a Prolog program is essentially an argument). Are you trying to check whether a theory is consistent or whether an argument is valid?
There are systems to check automatically whether an argument is valid; they are called theorem provers. You can't automatically check whether a theory is consistent except for a restricted class of theories. What you have to do if you want to check the consistency of a theory A is map A onto a theory B that you already believe is consistent, and prove that A is consistent if B is. That kind of mapping requires creativity and can't be done automatically.
On the other hand, it's possible that most theories expressed in philosophy books that can be formalized at all are in the class where consistency is decidable, but I don't know of any existing software system to do this. Maybe you could adapt a theorem prover to the task.
And then you run into problems with modality, temporal relations and other logical operators that don't follow the normal rules of predicate logic. I suspect that most theories presented in philosophy books make use of these sorts of things, so you will need a theory-checker that handles them correctly.
Natural language is a notoriously complicated affair. For thousands of years, linguists have been studying grammars, making claims about it, and working in tandem with or as logicians to understand the how's, what's why's, etc. Any challenging work of philosophy is not only using natural language, but is pushing the boundaries of what it is capable of, perhaps, by introducing neologisms or challenging conventional definitions.
That being said, there are many properties of language that do not lend themselves well to encoding claims. First, and most importantly is ambiguity. When reading a text, it's just a fact of life that you will be greeted with semantics that is uncertain. Why is that important? Because natural language is about sharing semantics. How are you supposed to encode the notion of transcendental idealism into a formal logic to preserve all of the meanings and relations that are intended (and unintended) in Critique of Pure Reason? I struggle even understanding passages of it, let alone trying to codifying it into a syntax that can be compiled or interpreted. If you have any experience diagramming sentences, you'll be acquainted with the difficulty that even one challenging compound-complex sentence can present, let alone a volume by Kant translated from his outdated German into contemporary English. In fact, there's a topic called the indeterminancy of translation that challenges the idea that translation can be done well at all (though it obviously seems to happen all the time).
For instance, there are aspects of language that are often difficult to even detect at all. Pragmatics is the study of how sometimes language communicates above and beyond the literal text. Sometimes 'yes' is 'no', and sometimes 'no' is 'yes'. There's an entire discipline known as literary theory devoted to such matters, since philosophical texts are often read within the implications of their historical period and with the biography of the author in mind.
It should be mentioned that while your goal is ambitious, and probably not possible, it is shared by others, such as Leibniz who invented the Characteristica universalis with the same goal. What if we could create the perfect artificial language to translate arguments into a calculus so that all might objectively agree of the outcome? It's a great idea, but the reality is that even in the clearest of philosophical arguments made in informal logic, there's very little possibility that such text could be converted into a formal system that once computed would yield practical results. Natural language is just too complex for that, though piecewise, there are companies like Cyc that attempt to codify and automate knowledge of domains in a limited fashion.
You may make a first attempt with Spinoza's Ethics.
Spinoza structures his book according to
As an example see the first
Definitions
I. By that which is self-caused, I mean that of which the essence involves existence, or that of which the nature is only conceivable as existent.
II. A thing is called finite after its kind, when it can be limited by another thing of the same nature; for instance, a body is called finite because we always conceive another greater body. So, also, a thought is limited by another thought, but a body is not limited by thought, nor a thought by body.
III. By substance, I mean that which is in itself, and is conceived through itself: in other words, that of which a conception can be formed independently of any other conception.
IV. By attribute, I mean that which the intellect perceives as constituting the essence of substance.
Axioms
I. Everything which exists, exists either in itself or in something else.
II. That which cannot be conceived through anything else must be conceived through itself.
III. From a given definite cause an effect necessarily follows ; and, on the other hand, if no definite cause be granted, it is impossible that an effect can follow.
IV. The knowledge of an effect depends on and involves the knowledge of a cause.
Propositions
Prop. I. Substance is by nature prior to its modifications.
Proof.—This is clear from Deff. iii. and v.
Prop. II. Two substances, whose attributes are different, have nothing in common.
Proof.—Also evident from Def. iii. For each must exist in itself, and be conceived through itself ; in other words, the conception of one does not imply the conception of the other.
Prop. III. Things which have nothing in common cannot be one the cause of the other.
Proof.—If they have nothing in common, it follows that one cannot be apprehended by means of the other (Ax. v.), and, therefore, one cannot be the cause of the other (Ax. iv.). Q.E.D.
Prop. IV. Two or more distinct things are distinguished one from the other, either by the difference of the attributes of the substances, or by the difference of their modifications.
Proof.—Everything which exists, exists either in itself or in something else (Ax. i.),—that is (by Deff. iii. and v.), nothing is granted in addition to the understanding, except substance and its modifications. Nothing is, therefore, given besides the understanding, by which several things may be distinguished one from the other, except the substances, or, in other words (see Ax. iv.), their attributes and modifications. Q.E.D.
The book has the subtitle 'Ordine Geometrico demonstrata' (Proofs according to the method of geometry).
I am unsure what the result of formalization in Prolog will be, but I am curious.
