How Does Proofs and Types Explore the Foundations of Mathematics and Logic?

  • Thread starter Thread starter Kevin_Axion
  • Start date Start date
  • Tags Tags
    Book Proofs
AI Thread Summary
The discussion centers on the free book "Proofs and Types" by Jean-Yves Girard, which explores the connections between logic and mathematics through the lens of type theory. The text emphasizes the significance of proofs as mathematical objects and their relationship to types in programming languages. It is noted that the book has been translated and includes appendices by Paul Taylor and Yves Lafont, enhancing its accessibility. The publication history indicates it was first released in 1989 and has undergone several reprints, including a web version in 2003. Overall, "Proofs and Types" serves as a foundational resource for understanding the interplay between logic and mathematical proofs.
Kevin_Axion
Messages
912
Reaction score
3
A Free Book "Proofs and Types"

http://www.mpi-sws.org/~dreyer/tor/papers/girard.pdf
Proofs and Types
Jean-Yves Girard
Translated and with appendices by:
Paul Taylor
Yves Lafont
Cambridge University Press
New York
Melbourne
New Rochelle
Sydney


Published by the Press Syndicate of the University of Cambridge
The Pitt Building, Trumpington Street, Cambridge CB2 1RP
32 East 57th Streey, New York, NY 10022, USA
10 Stamford Road, Oakleigh, Melbourne 3166, Australia

© Cambridge University Press, 1989
First Published 1989
Reprinted with minor corrections 1990
Reprinted for the Web 2003
Originally printed in Great Britain at the University Press, Cambridge
British Library Cataloguing in Publication Data available
Library of Congress Cataloguing in Publication Data available
ISBN 0 521 37181 3
 
Mathematics news on Phys.org


By using spherical coordinates how can we get the volume of a right circular cylinder with radius a and height h
 
Thread 'Video on imaginary numbers and some queries'
Hi, I was watching the following video. I found some points confusing. Could you please help me to understand the gaps? Thanks, in advance! Question 1: Around 4:22, the video says the following. So for those mathematicians, negative numbers didn't exist. You could subtract, that is find the difference between two positive quantities, but you couldn't have a negative answer or negative coefficients. Mathematicians were so averse to negative numbers that there was no single quadratic...
Thread 'Unit Circle Double Angle Derivations'
Here I made a terrible mistake of assuming this to be an equilateral triangle and set 2sinx=1 => x=pi/6. Although this did derive the double angle formulas it also led into a terrible mess trying to find all the combinations of sides. I must have been tired and just assumed 6x=180 and 2sinx=1. By that time, I was so mindset that I nearly scolded a person for even saying 90-x. I wonder if this is a case of biased observation that seeks to dis credit me like Jesus of Nazareth since in reality...
Thread 'Imaginary Pythagoras'
I posted this in the Lame Math thread, but it's got me thinking. Is there any validity to this? Or is it really just a mathematical trick? Naively, I see that i2 + plus 12 does equal zero2. But does this have a meaning? I know one can treat the imaginary number line as just another axis like the reals, but does that mean this does represent a triangle in the complex plane with a hypotenuse of length zero? Ibix offered a rendering of the diagram using what I assume is matrix* notation...

Similar threads

Replies
7
Views
3K
Replies
9
Views
4K
Back
Top