Logics and ontologies for portuguese

We may now construct a machine to do the work of this computer

Computing is normally done by writing certain symbols on paper

This is in accordance with experience. We cannot tell at a glance whether 9999999999999999 and 999999999999999 are the same

It is always possible for the computer to break off from his work, to go away and forget all about it, and later to come back and go on with it. If he does this he must leave a note of instructions (written in some standard form) explaining how the work is to be continued. This note is the counterpart of the 'state of mind'.

When detached from the local conditions of enunciations, the representation gains the form of an universal truth, the authority of evidences, of what needs no explanations.

EAL1: Functionally Tested

EAL2: Structurally Tested

EAL3: Methodically Tested and Checked,

EAL4: Methodically Designed, Tested, and Reviewed,

EAL5: Semiformally Designed and Tested,

EAL6: Semiformally Verified Design and Tested,

EAL7: Formally Verified Design and Tested.

(CCMB-2009-07-003)

IT products and protection profiles which earns a Common Criteria certificate can be procured or used without the need for further evaluation.

So, having for the moment suspended all rational disbelief, let us suppose that the programmer gets the message 'VERIFIED.' And let us suppose further that the message does not result from a failure on the part of the verifying system. What does the programmer know? He knows that his program is formally, logically, provably, certifiably correct. He does not know, however, to what extent it is reliable, dependable, trustworthy, safe; he does not know within what limits it will work; he does not know what happens when it exceeds those limits. And yet he has that mystical stamp of approval: 'VERIFIED.' We can almost see the iceberg looming in the background over the unsinkable ship." (DeMillo, Lipton, Perlis, 1979)

“Donald Knuth of Stanford University speculates that although Rabin's example has no immediate new applications, once a way to calculate something is found, someone always finds a use for it. (...) He believes, however, that the primary impact of Rabin's result is esthetic rather than practical. And on the grounds of esthetics, the contention begins.” (Kolata,1976)

Localizing Math

Isabel Cafezeiro (UFF)

Ivan da Costa Marques (UFRJ)

Isabel Cafezeiro

Ivan da Costa Marques

2011

Salto mortale

It is natural, now, to think of there being connected with a sign (name, combination of words, letter), besides that to which the sign refers, which may be called the reference of the sign, also what I should like to call the sense of the sign, wherein the mode of presentation is contained. (...) The reference of 'evening star' would be the same as that of 'morning star,' but not the sense.

HCTE

Ciências & Humanidades

all we need is to restore some part, no matter how small, of what we have taken away. In the case of the epistemological chasm the first reasonable step is to remember that the chasm was filled with SOME empirical material, whether ideational or sensational, which performed SOME bridging function and saved us from the mortal leap. Restoring thus the indispensable modicum of reality to the matter of our discussion, we find our abstract treatment genuinely useful. We escape entanglement with special cases without at the same time falling into gratuitous paradoxes.

For we first empty idea, object and intermediaries of all their particularities, in order to retain only a general scheme, and then we consider the latter only in its function of giving a result, and not in its character of being a process. In this treatment the intermediaries shrivel into the form of a mere space of separation, while the idea and object retain only the logical distinctness of being the end-terms that are separated.

2) Conjunctural situations have directly influence in the conformation of what is said "technical"

Simpósio Nacional de História

Turing computability is intrinsically persuasive.”

“λ-definability is not intrinsically persuasive.”

“General recursiveness scarcely so.

The most satisfactory way, in my opinion, is that of reducing the concept of finite procedure to that of a machine with a finite number of parts, as has been done by the British mathematician Turing

1) Asymmetric power relations are strengthened in what is said "technical"

Encontro Luso Brasileiro de História da Matemática

Circulating Reference

On computable numbers, with an application to the Entscheidungsproblem

1936

Although not proved in a formal system, Turing’s proof is as rigorous as many in mathematics. Gandy observed, “Turing’s analysis does much more than provide an argument for” Turing’s Thesis, “it proves a theorem.” (Soare, 1996)

An ethnographer !!!

scientiarum historia

When 'objectivity' faces the world of life...

1977

Michael Rabin

1960 probabilistic automata

1975 the same idea for adapting Gary Miller polynomial time test for primality, that, although deterministic, depended on an unproven assumption (extended Riemann hypothesis).

Texas

interest payments

$293,539.16

$331,667.00

$334,858.18

Digital

$331,559.38

With the idea of using probability and allowing the possibility of error, I took his test and made it into what’s now called a randomized algorithm, which today is the most efficient test for primality (…). My test is about eight times faster than theirs [R. Solovay and V. Strassen] and is what is now universally being used.

Weinberger answers: 'I'm willing to be convinced. Just show me one substantial example