Formally Deriving the Third Newton’s Law from a Pair of Nontrivial Assumptions in a Formal Axiomatic Theory “Sigma-V”

The article is devoted to hitherto never undertaken applying an almost unknown logically formalized axiomatic epistemology-and-axiology system called “Sigma-V” to the Third Newton’s Law of mechanics. The author has continued investigating the extraordinary (paradigm-breaking) hypothesis of formal-axiological interpreting Newton’s mathematical principles of natural philosophy and, thus, has arrived to discrete mathematical modeling a system of formal axiology of nature by extracting and systematical studying its proper algebraic aspect. Along with the proper algebraic machinery, the axiomatic (hypothetic-deductive) method is exploited in this investigation systematically. The research results are the followings. 1) The Third Newton’s Law of mechanics has been modeled by a formal-axiological equation of two-valued algebraic system of metaphysics as formal axiology. (Precise defining the algebraic system is provided.) The formal-axiological equation has been established (and examined) in this algebraic system by accurate computing compositions of relevant evaluation-functions. Precise tabular definitions of the evaluation-functions are given. 2) The wonderful formula representing the Third Newton’s Law (in the relevant physical interpretation of the formal theory Sigma-V) has been derived logically in Sigma-V from the presumption of a-priori-ness of knowledge. A precise axiomatic definition of the nontrivial notion “a-priori-ness of knowledge” is given. The formal derivation is implemented in strict accordance with the rigor standard of D. Hilbert’s formalism;hence, checking the formal derivation submitted in this article is not a difficult task. With respect to proper theoretical physics, the formal inference is a nontrivial scientific novelty which has not been discussed and published elsewhere yet.

Informal Logic： Between Logic and Epistemology

Nowadays researchers working in various fields study the issues of argument. They represent different approaches which distinguish with theoretical and practical comprehension of argument problems. Informal study of argument is one of the approaches. The key reason of its appearance was the criticism of formal logic in the late 20th century. Researchers consider the argument from the different point of view. Formal dialectics and pragma-dialectics were based on dialectics. Contemporary rhetorical theories of argument were created on the rhetorical grounds; theory of speech acts on the basis of practical philosophy etc.. This paper is devoted to some theoretical problems of informal logic which was formed on the logic background in the late 70＇s. In spite of numerous papers, books, and text-books on informal logic published over the last thirty years, logicians has not achieved consensus so far on many issues. Among the numerous problems are： what is the subject matter of informal logic？ Does informal logic belong to the realm of logic？ Is it applied epistemology？ What is a real argument？ And what are the criteria for evaluating of such arguments？

New method for hybrid multiple attribute decision-making problems with decision maker's aspiration level

How can we account for decision maker's aspiration level in multiple attribute decision-making problems? This is a question that has recently gained much scholarly attention. This study draws on the prospect theory and the Dempster-Shafer theory to propose a method that can resolve this issue. First, the precise and interval numbers and linguistic labels are compared, and then, the decision matrix is transformed into a prospect decision matrix on the basis of decision maker's aspiration level. Second, the Dempster-Shafer theory is applied to aggregate the prospect values of all alternatives on each attribute using their prospect belief intervals. Third, the orders of alternatives are obtained for all decision methods by comparing prospect belief intervals. Final, the effectiveness and feasibility of the proposed method are demonstrated by using an illustrative example. © 1990-2011 Beijing Institute of Aerospace Information.

Decision Making as Theorem Proving

We present a method for using type theory to solve decision making problem. Our method is based on the view that decision making is a special kind of theorem proving activity. An isomorphism between problems and types, and solutions and programs has been established to support this view which is much similar to the Curry-Howard isomorphism between propositions and types, and proofs and programs. To support our method, a proof development system called PowerEpsilon has been developed, and the synthesis of a decision procedure for validity of first-order propositional logic is discussed to show the power of the system.

The Binary Logic of the Compilation of the Ecological Environment Code and Its Unfolding

The Ecological Environment Code,as a significant legal instrument for the evolution of ecological civilization,possesses both substantive and formal dimensions.First,it aims to serve the national ecological civilization strategy.Second,it elucidates potential pathways for legal interpretation,development of legal rules,and promotion of judicial governance,restraining arbitrary behavior and disorder while facilitating systemic cohesion.The compilation of the Ecological Environment Code unfolds through the main threads of substantive and formal logic.By prioritizing conservation,protection,and restoring the natural environment,resource management,pollution prevention,and ecological protection are coordinated,integrating legislation on ecological protection with management of natural resources and pollution prevention to achieve both"harm avoidance"and"beneficial trends."Employing the formal logical main thread of the structure of the relationship between power and rights,we present four types of norms:ex post facto remedy,hazard prevention,risk prevention,and independent value selection.

A REVIEW AND PROSPECT OF READABLE MACHINE PROOFS FOR GEOMETRY THEOREMS

After half a century research, the mechanical theorem proving in geometries has become an active research topic in the automated reasoning field. This review involves three approaches on automated generating readable machine proofs for geometry theorems which include search methods, coordinate-free methods, and formal logic methods. Some critical issues about these approaches are also discussed. Furthermore, the authors propose three further research directions for the readable machine proofs for geometry theorems, including geometry inequalities, intelligent geometry softwares and machine learning.

Construction of the Model of the Lambda Calculus System with Algebraic Operators

A lambda system with algebraic operators,lambda-plus system,is introduced.After giving the definitions of the system,we present a sufficient condition for formulating a model of the system. Finally,a model of such system is constructed.