Set Theory and Logic


Recent Advances in Refutations and Validations Using Meth8 Modal Logic Model Checker © Colin James III 2016-2017 All Rights Reserved.

Authors: Colin James III

© Colin James III 2016-2017 All rights reserved. In applied and theoretical mathematics, assertions are categorized in alphabetical order as: axiom; conjecture; definition, entry; equation; expression; formula; functor; hypothesis; inequality; metatheorem; paradox; problem; proof; schema; system; theorem; and thesis. We evaluate 130 objects for 519 assertions to validate 156 as tautology and 363 as not (70%). We use Meth8 that is a modal logic checker in five models. The semantic content or predicate basis of some expressions on their face does not disqualify them from evaluation by Meth8 in classical modal logic. However, the rules of classical logic, as based on the corrected Square of Opposition by Meth8, apply to virtually any logic system. Consequently some numerical equations are mapped to classical logic as Meth8 scripts. The rationale for mapping quantifiers as modal operators is in the Appendix based on satisfiability and reproducability of validation of syllogisms. A table lists what was tested with separated results. The names are numbered in alphabetical order. Test results are Invalidated as Not Validated Tautology (nvt) or Validated as Tautology (vt). For a paradox, invalidated means it is not validated as true, that is, it is not a paradox or contradiction. The experimental tests used variables for 4 propositions, 4 theorems, and 11 propositions. The size of truth tables are respectively for 16-, 256-, and 2048- truth values. One formula of Popper in 250-characters processed in 125-steps instantly due to recent advances in look up table indexing. The Meth8 modal theorem prover implements the logic system variant VŁ4 which corrects the quaternary Ł4 of Łukasiewicz. There are two sets of truth values on the 2-tuple {00, 10, 01, 11} as respectively and . The model checker contains recent advances in parsing technology and is U.S. Patent Pending. The mapping of formulas into Meth8 script was performed by hand, checked, and tested for accuracy of intent. (A semi-automation of that process is underway.) The Meth8 script uses literals and connectives in one-character. Propositions are p-z, and theorems are A-B. The connectives for are <&; +; >; =). The negated connectives for are <\; -; <; @>. The operators for are <~; %; #>. Some expressions are adopted for clarity such as: (p=p) for true; (p@p) for false; and (xy). Def Axiom Sym Name Meaning 11 p=p T Tautology proof 00 p@p F Contradiction absurdum 01 %p>#p N Non-contingency truth 10 %p<#p C Contingency falsity The designated proof value is T tautology. Note the meaning of (%p>#p): a possibility of p implies the necessity of p; and some p implies all p. In other words, if a possibility of p then the necessity of p; and if some p then all p. This shows equivalence and interchangeability of respective modal operators and quantified operators, as proved in Appendix. For Meth8 an immediate further application to "validate as tautologous" is mapping sentences of natural language into logical formulas. The approach identifies parts of speech as nouns, verbs, and modifiers. These translate into logical symbols for literals, connectives, and operators. For example: the conjunction "and" becomes the connective "&"; and the modifier articles "the" and "a" become the modal box # and lozenge %. Expressions for consecutive sentences are linked by the imply connective to build paragraphs to form requirements documents.

Comments: 189 Pages.

Download: PDF

Submission history

[v1] 2017-11-10 10:13:03

Unique-IP document downloads: 117 times is a pre-print repository rather than a journal. Articles hosted may not yet have been verified by peer-review and should be treated as preliminary. In particular, anything that appears to include financial or legal advice or proposed medical treatments should be treated with due caution. will not be responsible for any consequences of actions that result from any form of use of any documents on this website.

Add your own feedback and questions here:
You are equally welcome to be positive or negative about any paper but please be polite. If you are being critical you must mention at least one specific error, otherwise your comment will be deleted as unhelpful.

comments powered by Disqus