View source for Blog:Formal theory, finite model and DL reasoner/Second Statement

HensonGraves:

The paradigm that I am suggesting is exactly the same one that is in John's diagram. For this audience I will stick to logician's terminology. Engineers develop artifacts which are naturally axiom sets even if they don't always recognize it. The axiom sets generate a theory depending on the logic the axiom set is embedded in. The axiom sets are finitely presented. The theory generated by the axiom set are the conclusions which can be derived from the axioms in the logic. As any axiom set or theory there are natural definitions of a valid model of the theory generated by the axiom set. Depending on the axiom set there may possibly be both finite or infinite models. Following John's diagram there are two general kinds of models, the ones in the physical world and simulation models. To me what is important in both cases is not finiteness of the model but its constructivity. This requires a lot more discussion which I will not do here. Following the usual logic paradigm you expect the reasoning to be "true" in all valid models, at least when the theory is sound.

For now only one more idea.

The axioms sets that engineers produce generally have a lot more valid models than the engineer intended. So a lot of practical engineering work is identifying the additional assumptions needed to constrain the valid models. One could view these additional assumptions as "context" for the axiom sets. That is in some domain all of these assumptions could be added automatically to a proof assistant (aka engineer's model development tool) without the axiom set developer even being aware of it. For example in the paper reference above we were modeling both the aircraft and its operational environment. For the axiom set to generate the 3D simulations that we produced we had to add an immense amount of assumptions about physics regarding aerodynamics, sensor performance etc.
{{wl-publish: 2018-02-05 12:35:06 -0500 | Ashkotin }}