scholarly journals The Gauge Integral Theory in HOL4

2013 ◽  
Vol 2013 ◽  
pp. 1-7 ◽  
Author(s):  
Zhiping Shi ◽  
Weiqing Gu ◽  
Xiaojuan Li ◽  
Yong Guan ◽  
Shiwei Ye ◽  
...  
Keyword(s):  
Dynamical Systems ◽  
Higher Order ◽  
Integral Theory ◽  
Order Logic ◽  
Cauchy Type ◽  
Lebesgue Integral ◽  
Higher Order Logic ◽  
Riemann Integral ◽  
Integrability Criterion ◽  
Class Of Functions

The integral is one of the most important foundations for modeling dynamical systems. The gauge integral is a generalization of the Riemann integral and the Lebesgue integral and applies to a much wider class of functions. In this paper, we formalize the operational properties which contain the linearity, monotonicity, integration by parts, the Cauchy-type integrability criterion, and other important theorems of the gauge integral in higher-order logic 4 (HOL4) and then use them to verify an inverting integrator. The formalized theorem library has been accepted by the HOL4 authority and will appear in HOL4 Kananaskis-9.

Measure Theory and Lebesgue Integration Theories

2015 ◽  
pp. 29-46
Keyword(s):  
Probability Theory ◽  
Measure Theory ◽  
Higher Order ◽  
Order Logic ◽  
Lebesgue Integral ◽  
Real Numbers ◽  
Convergence Theorems ◽  
Higher Order Logic ◽  
Lebesgue Integration

As discussed in the previous chapter, the fundamental theories of measure and Lebesgue integration are the prerequisites for the formalization of probability theory in higher-order logic. The scope of this chapter is primarily the formalization of these foundations. Both formalizations of measure theory and Lebesgue integral (Mhamdi, Hasan, & Tahar, 2011), presented in this chapter, are based on the extended-real numbers. This allows us to define sigma-finite and even infinite measures and handle extended-real-valued measurable functions. It also allows us to verify the properties of the Lebesgue integral and its convergence theorems for arbitrary functions. Therefore, the chapter begins with a description of the formalization of extended real numbers.

scholarly journals Closed Structure

2021 ◽  
Author(s):  
Peter Fritz ◽  
Harvey Lederman ◽  
Gabriel Uzquiano
Keyword(s):  
Formal Language ◽  
Syntactic Structure ◽  
Natural Extension ◽  
Propositional Attitudes ◽  
Higher Order ◽  
Order Logic ◽  
Bertrand Russell ◽  
Structured Propositions ◽  
Higher Order Logic ◽  
Closed Structure

AbstractAccording to the structured theory of propositions, if two sentences express the same proposition, then they have the same syntactic structure, with corresponding syntactic constituents expressing the same entities. A number of philosophers have recently focused attention on a powerful argument against this theory, based on a result by Bertrand Russell, which shows that the theory of structured propositions is inconsistent in higher order-logic. This paper explores a response to this argument, which involves restricting the scope of the claim that propositions are structured, so that it does not hold for all propositions whatsoever, but only for those which are expressible using closed sentences of a given formal language. We call this restricted principle Closed Structure, and show that it is consistent in classical higher-order logic. As a schematic principle, the strength of Closed Structure is dependent on the chosen language. For its consistency to be philosophically significant, it also needs to be consistent in every extension of the language which the theorist of structured propositions is apt to accept. But, we go on to show, Closed Structure is in fact inconsistent in a very natural extension of the standard language of higher-order logic, which adds resources for plural talk of propositions. We conclude that this particular strategy of restricting the scope of the claim that propositions are structured is not a compelling response to the argument based on Russell’s result, though we note that for some applications, for instance to propositional attitudes, a restricted thesis in the vicinity may hold some promise.

Adapting functional programs to higher order logic

2008 ◽  
Vol 21 (4) ◽  
pp. 377-409 ◽  
Author(s):  
Scott Owens ◽  
Konrad Slind
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic

scholarly journals “How did the serpent of inconsistency enter Frege’s paradise?”

2019 ◽  
pp. 411-436
Author(s):  
Crispin Wright
Keyword(s):  
Cardinal Number ◽  
Ordinal Number ◽  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Indefinite Extensibility ◽  
Basic Law ◽  
Per Se

The paper explores the alleged connection between indefinite extensibility and the classic paradoxes of Russell, Burali-Forti, and Cantor. It is argued that while indefinite extensibility is not per se a source of paradox, there is a degenerate subspecies—reflexive indefinite extensibility—which is. The result is a threefold distinction in the roles played by indefinite extensibility in generating paradoxes for the notions of ordinal number, cardinal number, and set respectively. Ordinal number, intuitively understood, is a reflexively indefinitely extensible concept. Cardinal number is not. And Set becomes so only in the setting of impredicative higher-order logic—so that Frege’s Basic Law V is guilty at worst of partnership in crime, rather than the sole offender.

scholarly journals Making Automatic Theorem Provers more Versatile

10.29007/n6j7 ◽  
2018 ◽  
Author(s):  
Simon Cruanes
Keyword(s):  
Higher Order ◽  
Order Logic ◽  
Higher Order Logic ◽  
Research Directions ◽  
First Order ◽  
Theorem Provers ◽  
Smt Solvers ◽  
Automatic Theorem Provers ◽  
Automatic Theorem

We argue that automatic theorem provers should become more versatile and should be able to tackle problems expressed in richer input formats. Salient research directions include (i) developing tight combinations of SMT solvers and first-order provers; (ii) adding better handling of theories in first-order provers; (iii) adding support for inductive proving; (iv) adding support for user-defined theories and functions; and (v) bringing to the provers some basic abilities to deal with logics beyond first-order, such as higher-order logic.

Sign in / Sign up

Export Citation Format

Share Document